helm/software/matita/tests/reduction_new_preamble.ma

   1
   2 universe constraint Type[0] < Type[1].
   3
   4 ninductive exadecim : Type ≝
   5   x0: exadecim
   6 | x1: exadecim
   7 | x2: exadecim
   8 | x3: exadecim
   9 | x4: exadecim
  10 | x5: exadecim
  11 | x6: exadecim
  12 | x7: exadecim
  13 | x8: exadecim
  14 | x9: exadecim
  15 | xA: exadecim
  16 | xB: exadecim
  17 | xC: exadecim
  18 | xD: exadecim
  19 | xE: exadecim
  20 | xF: exadecim.
  21
  22 ninductive bool : Type ≝ true :bool | false : bool .
  23
  24 ndefinition eq_ex ≝
  25 λe1,e2:exadecim.
  26  match e1 with
  27   [ x0 ⇒ match e2 with [ x0 ⇒ true  | _ ⇒ false ]
  28   | x1 ⇒ match e2 with [ x1 ⇒ true  | _ ⇒ false ]
  29   | x2 ⇒ match e2 with [ x2 ⇒ true  | _ ⇒ false ]
  30   | x3 ⇒ match e2 with [ x3 ⇒ true  | _ ⇒ false ]
  31   | x4 ⇒ match e2 with [ x4 ⇒ true  | _ ⇒ false ]
  32   | x5 ⇒ match e2 with [ x5 ⇒ true  | _ ⇒ false ]
  33   | x6 ⇒ match e2 with [ x6 ⇒ true  | _ ⇒ false ]
  34   | x7 ⇒ match e2 with [ x7 ⇒ true  | _ ⇒ false ]
  35   | x8 ⇒ match e2 with [ x8 ⇒ true  | _ ⇒ false ]
  36   | x9 ⇒ match e2 with [ x9 ⇒ true  | _ ⇒ false ]
  37   | xA ⇒ match e2 with [ xA ⇒ true  | _ ⇒ false ]
  38   | xB ⇒ match e2 with [ xB ⇒ true  | _ ⇒ false ]
  39   | xC ⇒ match e2 with [ xC ⇒ true  | _ ⇒ false ]
  40   | xD ⇒ match e2 with [ xD ⇒ true  | _ ⇒ false ]
  41   | xE ⇒ match e2 with [ xE ⇒ true  | _ ⇒ false ]
  42   | xF ⇒ match e2 with [ xF ⇒ true  | _ ⇒ false ]
  43   ].
  44
  45 ndefinition succ_ex ≝
  46 λe:exadecim.
  47  match e with
  48   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
  49   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
  50
  51
  52 nrecord byte8 : Type ≝
  53  {
  54  b8h: exadecim;
  55  b8l: exadecim
  56  }.
  57
  58 notation "〈x,y〉" non associative with precedence 80
  59  for @{ 'mk_byte8 $x $y }.
  60 interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
  61
  62 ndefinition andb ≝ λa,b.match a with [ true ⇒ b | _ ⇒ false ].
  63
  64 ndefinition eq_b8 ≝ λb1,b2:byte8.andb (eq_ex (b8h b1) (b8h b2))  (eq_ex (b8l b1) (b8l b2)).
  65 ndefinition succ_b8 ≝
  66 λb:byte8.match eq_ex (b8l b) xF with
  67  [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
  68  | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
  69
  70 nrecord word16 : Type ≝
  71  {
  72  w16h: byte8;
  73  w16l: byte8
  74  }.
  75
  76 (* \langle \rangle *)
  77 notation "〈x:y〉" non associative with precedence 80
  78  for @{ 'mk_word16 $x $y }.
  79 interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
  80
  81 ndefinition succ_w16 ≝
  82 λw:word16.
  83   match eq_b8 (w16l w) (mk_byte8 xF xF) with
  84  [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w))
  85  | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ].
  86
  87 ninductive eq (A:Type) (a:A) : A → Prop ≝ refl_eq : eq A a a.
  88
  89 interpretation "aa" 'eq t a b = (eq t a b).
  90