]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/match_inference.ma
init_copy init_match
[helm.git] / matita / matita / tests / match_inference.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16
17 inductive pos: Set \def
18 | one : pos
19 | next : pos \to pos.
20
21 inductive nat:Set \def
22 | O : nat
23 | S : nat \to nat.
24
25 definition pos2nat : pos \to nat  \def 
26      \lambda x:pos . match x with  
27       [ one \Rightarrow O 
28       | (next z) \Rightarrow O]. 
29
30 inductive empty (x:nat) : nat \to Set \def .
31
32 definition empty2nat : (empty O O) \to nat  \def
33   \lambda x : (empty O O). S (match x in empty with []).
34
35 inductive le (n:nat) : nat \to Prop \def
36   | le_n : le n n
37   | le_S : \forall m:nat. le n m \to le n (S m).
38
39 inductive True : Prop \def
40  I : True.
41
42 definition r : True \def
43  match (le_n O) with
44   [ le_n \Rightarrow I
45   | (le_S y p') \Rightarrow I ].
46
47 inductive Prod (A,B:Set): Set \def
48 pair : A \to B \to Prod A B.
49
50 definition fst : \forall A,B:Set. (Prod A B) \to A \def
51 \lambda A,B:Set. \lambda p:(Prod A B). match p with
52 [(pair a b) \Rightarrow a].