]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/reduction_new_preamble.ma
splitting files
[helm.git] / matita / 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