helm/matita/tests/match_inference.ma

   1 set "baseuri" "cic:/matita/tests/match_inference/".
   2
   3 inductive pos: Set \def
   4 | one : pos
   5 | next : pos \to pos.
   6
   7 inductive nat:Set \def
   8 | O : nat
   9 | S : nat \to nat.
  10
  11 definition pos2nat : pos \to nat  \def
  12      \lambda x:pos . match x with
  13       [ one \Rightarrow O
  14       | (next z) \Rightarrow O].
  15
  16 inductive empty (x:nat) : nat \to Set \def .
  17
  18 definition empty2nat : (empty O O) \to nat  \def
  19   \lambda x : (empty O O). S (match x in empty with []).
  20
  21 inductive le (n:nat) : nat \to Prop \def
  22   | le_n : le n n
  23   | le_S : \forall m:nat. le n m \to le n (S m).
  24
  25 inductive True : Prop \def
  26  I : True.
  27
  28 definition r : True \def
  29  match (le_n O) with
  30   [ le_n \Rightarrow I
  31   | (le_S y p') \Rightarrow I ].
  32
  33 inductive Prod (A,B:Set): Set \def
  34 pair : A \to B \to Prod A B.
  35
  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].