helm/matita/tests/coercions.ma

   1
   2 Inductive nat : Set \def
   3 | O : nat
   4 | S : nat \to nat.
   5
   6 Inductive list (A:Set) : Set \def
   7 | nil : list A
   8 | cons : A \to list A \to list A.
   9
  10 Inductive bool: Set \def
  11 | true : bool
  12 | false : bool.
  13
  14
  15
  16
  17 let rec len (A:Set)(l:list A) on l : nat \def
  18  match l:list with [
  19    nil \Rightarrow O
  20  | (cons e tl) \Rightarrow (S (len A tl))].
  21
  22 let rec plus (n,m:nat) : nat \def
  23  match n:nat with [
  24    O \Rightarrow m
  25  | (S x) \Rightarrow (S (plus x m)) ].
  26
  27 let rec is_zero (n:nat) : bool \def
  28   match n:nat with [
  29     O \Rightarrow true
  30   | (S x) \Rightarrow false].
  31
  32 let rec nat_eq_dec (n,m:nat) : bool \def
  33   match n:nat with [
  34     O \Rightarrow
  35          match m:nat with [
  36            O \Rightarrow true
  37          | (S x) \Rightarrow false]
  38   | (S x) \Rightarrow
  39              match m:nat with [
  40                O \Rightarrow false
  41              | (S y) \Rightarrow (nat_eq_dec x y)]
  42   ].
  43
  44
  45 Coercion is_zero.
  46 Coercion len.
  47
  48 Print Coer.
  49 Print Env.
  50