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:pos) : nat  \def
  16   match x with
  17   [ one \Rightarrow (S O)
  18   | (next z) \Rightarrow S (pos2nat z)].
  19
  20 let rec nat2int (x:nat) :int \def
  21   match x with
  22   [ O \Rightarrow positive O
  23   | (S z) \Rightarrow positive (S z)].
  24
  25 coercion pos2nat.
  26
  27 coercion nat2int.
  28
  29 let rec plus x y : int \def
  30   match x with
  31   [ (positive n) \Rightarrow x
  32   | (negative z) \Rightarrow y].
  33
  34 theorem a: plus O one.
  35
  36
  37
  38
  39
  40
  41
  42
  43
  44