1 set "baseuri" "cic:/matita/tests/match_inference/".
3 inductive pos: Set \def
11 definition pos2nat : pos \to nat \def
12 \lambda x:pos . match x with
14 | (next z) \Rightarrow O].
16 inductive empty (x:nat) : nat \to Set \def .
18 definition empty2nat : (empty O O) \to nat \def
19 \lambda x : (empty O O). S (match x in empty with []).
21 inductive le (n:nat) : nat \to Prop \def
23 | le_S : \forall m:nat. le n m \to le n (S m).
25 inductive True : Prop \def
28 definition r : True \def
31 | (le_S y p') \Rightarrow I ].
33 inductive Prod (A,B:Set): Set \def
34 pair : A \to B \to Prod A B.
36 definition fst : \forall A,B:Set. (Prod A B) \to A \def
37 \lambda A,B:Set. \lambda p:(Prod A B). match p with
38 [(pair a b) \Rightarrow a].