1 | open Preamble |
---|
2 | |
---|
3 | open Hints_declaration |
---|
4 | |
---|
5 | open Core_notation |
---|
6 | |
---|
7 | open Pts |
---|
8 | |
---|
9 | open Logic |
---|
10 | |
---|
11 | open Relations |
---|
12 | |
---|
13 | type nat = |
---|
14 | | O |
---|
15 | | S of nat |
---|
16 | |
---|
17 | (** val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **) |
---|
18 | let rec nat_rect_Type4 h_O h_S = function |
---|
19 | | O -> h_O |
---|
20 | | S x_565 -> h_S x_565 (nat_rect_Type4 h_O h_S x_565) |
---|
21 | |
---|
22 | (** val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **) |
---|
23 | let rec nat_rect_Type3 h_O h_S = function |
---|
24 | | O -> h_O |
---|
25 | | S x_573 -> h_S x_573 (nat_rect_Type3 h_O h_S x_573) |
---|
26 | |
---|
27 | (** val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **) |
---|
28 | let rec nat_rect_Type2 h_O h_S = function |
---|
29 | | O -> h_O |
---|
30 | | S x_577 -> h_S x_577 (nat_rect_Type2 h_O h_S x_577) |
---|
31 | |
---|
32 | (** val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **) |
---|
33 | let rec nat_rect_Type1 h_O h_S = function |
---|
34 | | O -> h_O |
---|
35 | | S x_581 -> h_S x_581 (nat_rect_Type1 h_O h_S x_581) |
---|
36 | |
---|
37 | (** val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **) |
---|
38 | let rec nat_rect_Type0 h_O h_S = function |
---|
39 | | O -> h_O |
---|
40 | | S x_585 -> h_S x_585 (nat_rect_Type0 h_O h_S x_585) |
---|
41 | |
---|
42 | (** val nat_inv_rect_Type4 : |
---|
43 | nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **) |
---|
44 | let nat_inv_rect_Type4 hterm h1 h2 = |
---|
45 | let hcut = nat_rect_Type4 h1 h2 hterm in hcut __ |
---|
46 | |
---|
47 | (** val nat_inv_rect_Type3 : |
---|
48 | nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **) |
---|
49 | let nat_inv_rect_Type3 hterm h1 h2 = |
---|
50 | let hcut = nat_rect_Type3 h1 h2 hterm in hcut __ |
---|
51 | |
---|
52 | (** val nat_inv_rect_Type2 : |
---|
53 | nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **) |
---|
54 | let nat_inv_rect_Type2 hterm h1 h2 = |
---|
55 | let hcut = nat_rect_Type2 h1 h2 hterm in hcut __ |
---|
56 | |
---|
57 | (** val nat_inv_rect_Type1 : |
---|
58 | nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **) |
---|
59 | let nat_inv_rect_Type1 hterm h1 h2 = |
---|
60 | let hcut = nat_rect_Type1 h1 h2 hterm in hcut __ |
---|
61 | |
---|
62 | (** val nat_inv_rect_Type0 : |
---|
63 | nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **) |
---|
64 | let nat_inv_rect_Type0 hterm h1 h2 = |
---|
65 | let hcut = nat_rect_Type0 h1 h2 hterm in hcut __ |
---|
66 | |
---|
67 | (** val nat_discr : nat -> nat -> __ **) |
---|
68 | let nat_discr x y = |
---|
69 | Logic.eq_rect_Type2 x |
---|
70 | (match x with |
---|
71 | | O -> Obj.magic (fun _ dH -> dH) |
---|
72 | | S a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
73 | |
---|
74 | (** val pred : nat -> nat **) |
---|
75 | let pred = function |
---|
76 | | O -> O |
---|
77 | | S p -> p |
---|
78 | |
---|
79 | (** val plus : nat -> nat -> nat **) |
---|
80 | let rec plus n m = |
---|
81 | match n with |
---|
82 | | O -> m |
---|
83 | | S p -> S (plus p m) |
---|
84 | |
---|
85 | (** val times : nat -> nat -> nat **) |
---|
86 | let rec times n m = |
---|
87 | match n with |
---|
88 | | O -> O |
---|
89 | | S p -> plus m (times p m) |
---|
90 | |
---|
91 | (** val minus : nat -> nat -> nat **) |
---|
92 | let rec minus n m = |
---|
93 | match n with |
---|
94 | | O -> O |
---|
95 | | S p -> |
---|
96 | (match m with |
---|
97 | | O -> S p |
---|
98 | | S q -> minus p q) |
---|
99 | |
---|
100 | open Bool |
---|
101 | |
---|
102 | (** val eqb : nat -> nat -> Bool.bool **) |
---|
103 | let rec eqb n m = |
---|
104 | match n with |
---|
105 | | O -> |
---|
106 | (match m with |
---|
107 | | O -> Bool.True |
---|
108 | | S q -> Bool.False) |
---|
109 | | S p -> |
---|
110 | (match m with |
---|
111 | | O -> Bool.False |
---|
112 | | S q -> eqb p q) |
---|
113 | |
---|
114 | (** val leb : nat -> nat -> Bool.bool **) |
---|
115 | let rec leb n m = |
---|
116 | match n with |
---|
117 | | O -> Bool.True |
---|
118 | | S p -> |
---|
119 | (match m with |
---|
120 | | O -> Bool.False |
---|
121 | | S q -> leb p q) |
---|
122 | |
---|
123 | (** val min : nat -> nat -> nat **) |
---|
124 | let min n m = |
---|
125 | match leb n m with |
---|
126 | | Bool.True -> n |
---|
127 | | Bool.False -> m |
---|
128 | |
---|
129 | (** val max : nat -> nat -> nat **) |
---|
130 | let max n m = |
---|
131 | match leb n m with |
---|
132 | | Bool.True -> m |
---|
133 | | Bool.False -> n |
---|
134 | |
---|