helm/matita/tests/coercions.ma

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