]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/coercions.ma
moogle.html is now generated, it do not needs to be in CVS
[helm.git] / 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