helm/matita/tests/match_inference.ma

   1 inductive pos: Set \def
   2 | one : pos
   3 | next : pos \to pos.
   4
   5 inductive nat:Set \def
   6 | O : nat
   7 | S : nat \to nat.
   8
   9 definition pos2nat : pos \to nat  \def
  10      \lambda x:pos . match x with
  11       [ one \Rightarrow O
  12       | (next z) \Rightarrow O].
  13
  14 inductive empty (x:nat) : nat \to Set \def .
  15
  16 definition empty2nat : (empty O O) \to nat  \def
  17   \lambda x : (empty O O). S (match x in empty with []).
  18
  19 inductive le (n:nat) : nat \to Prop \def
  20   | le_n : le n n
  21   | le_S : \forall m:nat. le n m \to le n (S m).
  22
  23 inductive True : Prop \def
  24  I : True.
  25
  26 definition r : True \def
  27  match (le_n O) with
  28   [ le_n \Rightarrow I
  29   | (le_S y p') \Rightarrow I ].