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 inductive empty : Set \def .
  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 definition empty2nat : empty \to nat  \def
  17   \lambda x : empty . S (match x in empty with []).