helm/matita/tests/coercions.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 int: Set \def
  10 | positive: nat \to int
  11 | negative : nat \to int.
  12
  13 inductive empty : Set \def .
  14
  15 let rec pos2nat x \def
  16   match x with
  17   [ one \Rightarrow (S O)
  18   | (next z) \Rightarrow S (pos2nat z)].
  19
  20 definition nat2int \def \lambda x. positive x.
  21
  22 coercion pos2nat.
  23
  24 coercion nat2int.
  25
  26 definition fst \def \lambda x,y:int.x.
  27 alias symbol "eq" (instance 0) = "leibnitz's equality".
  28
  29 theorem a: fst O one = fst (positive O) (next one).
  30 reflexivity.
  31 qed.