[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Hints_declaration |
---|
| 4 | |
---|
| 5 | open Core_notation |
---|
| 6 | |
---|
| 7 | open Pts |
---|
| 8 | |
---|
| 9 | open Logic |
---|
| 10 | |
---|
| 11 | open Types |
---|
| 12 | |
---|
| 13 | open Relations |
---|
| 14 | |
---|
| 15 | open Bool |
---|
| 16 | |
---|
| 17 | type deqSet = |
---|
| 18 | __ -> __ -> Bool.bool |
---|
| 19 | (* singleton inductive, whose constructor was mk_DeqSet *) |
---|
| 20 | |
---|
| 21 | (** val deqSet_rect_Type4 : |
---|
| 22 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
[2773] | 23 | let rec deqSet_rect_Type4 h_mk_DeqSet x_3369 = |
---|
| 24 | let eqb = x_3369 in h_mk_DeqSet __ eqb __ |
---|
[2601] | 25 | |
---|
| 26 | (** val deqSet_rect_Type5 : |
---|
| 27 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
[2773] | 28 | let rec deqSet_rect_Type5 h_mk_DeqSet x_3371 = |
---|
| 29 | let eqb = x_3371 in h_mk_DeqSet __ eqb __ |
---|
[2601] | 30 | |
---|
| 31 | (** val deqSet_rect_Type3 : |
---|
| 32 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
[2773] | 33 | let rec deqSet_rect_Type3 h_mk_DeqSet x_3373 = |
---|
| 34 | let eqb = x_3373 in h_mk_DeqSet __ eqb __ |
---|
[2601] | 35 | |
---|
| 36 | (** val deqSet_rect_Type2 : |
---|
| 37 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
[2773] | 38 | let rec deqSet_rect_Type2 h_mk_DeqSet x_3375 = |
---|
| 39 | let eqb = x_3375 in h_mk_DeqSet __ eqb __ |
---|
[2601] | 40 | |
---|
| 41 | (** val deqSet_rect_Type1 : |
---|
| 42 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
[2773] | 43 | let rec deqSet_rect_Type1 h_mk_DeqSet x_3377 = |
---|
| 44 | let eqb = x_3377 in h_mk_DeqSet __ eqb __ |
---|
[2601] | 45 | |
---|
| 46 | (** val deqSet_rect_Type0 : |
---|
| 47 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
[2773] | 48 | let rec deqSet_rect_Type0 h_mk_DeqSet x_3379 = |
---|
| 49 | let eqb = x_3379 in h_mk_DeqSet __ eqb __ |
---|
[2601] | 50 | |
---|
| 51 | type carr = __ |
---|
| 52 | |
---|
| 53 | (** val eqb : deqSet -> __ -> __ -> Bool.bool **) |
---|
| 54 | let rec eqb xxx = |
---|
| 55 | let yyy = xxx in yyy |
---|
| 56 | |
---|
| 57 | (** val deqSet_inv_rect_Type4 : |
---|
| 58 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 59 | let deqSet_inv_rect_Type4 hterm h1 = |
---|
| 60 | let hcut = deqSet_rect_Type4 h1 hterm in hcut __ |
---|
| 61 | |
---|
| 62 | (** val deqSet_inv_rect_Type3 : |
---|
| 63 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 64 | let deqSet_inv_rect_Type3 hterm h1 = |
---|
| 65 | let hcut = deqSet_rect_Type3 h1 hterm in hcut __ |
---|
| 66 | |
---|
| 67 | (** val deqSet_inv_rect_Type2 : |
---|
| 68 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 69 | let deqSet_inv_rect_Type2 hterm h1 = |
---|
| 70 | let hcut = deqSet_rect_Type2 h1 hterm in hcut __ |
---|
| 71 | |
---|
| 72 | (** val deqSet_inv_rect_Type1 : |
---|
| 73 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 74 | let deqSet_inv_rect_Type1 hterm h1 = |
---|
| 75 | let hcut = deqSet_rect_Type1 h1 hterm in hcut __ |
---|
| 76 | |
---|
| 77 | (** val deqSet_inv_rect_Type0 : |
---|
| 78 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 79 | let deqSet_inv_rect_Type0 hterm h1 = |
---|
| 80 | let hcut = deqSet_rect_Type0 h1 hterm in hcut __ |
---|
| 81 | |
---|
| 82 | (** val beqb : Bool.bool -> Bool.bool -> Bool.bool **) |
---|
| 83 | let beqb b1 b2 = |
---|
| 84 | match b1 with |
---|
| 85 | | Bool.True -> b2 |
---|
| 86 | | Bool.False -> Bool.notb b2 |
---|
| 87 | |
---|
| 88 | (** val deqBool : deqSet **) |
---|
| 89 | let deqBool = |
---|
| 90 | Obj.magic beqb |
---|
| 91 | |
---|
| 92 | (** val eq_option : |
---|
| 93 | deqSet -> __ Types.option -> __ Types.option -> Bool.bool **) |
---|
| 94 | let eq_option a a1 a2 = |
---|
| 95 | match a1 with |
---|
| 96 | | Types.None -> |
---|
| 97 | (match a2 with |
---|
| 98 | | Types.None -> Bool.True |
---|
| 99 | | Types.Some x -> Bool.False) |
---|
| 100 | | Types.Some a1' -> |
---|
| 101 | (match a2 with |
---|
| 102 | | Types.None -> Bool.False |
---|
| 103 | | Types.Some a2' -> eqb a a1' a2') |
---|
| 104 | |
---|
| 105 | (** val deqOption : deqSet -> deqSet **) |
---|
| 106 | let deqOption a = |
---|
| 107 | Obj.magic (eq_option a) |
---|
| 108 | |
---|
| 109 | (** val eq_pairs : |
---|
| 110 | deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> |
---|
| 111 | Bool.bool **) |
---|
| 112 | let eq_pairs a b p1 p2 = |
---|
| 113 | Bool.andb (eqb a p1.Types.fst p2.Types.fst) |
---|
| 114 | (eqb b p1.Types.snd p2.Types.snd) |
---|
| 115 | |
---|
| 116 | (** val deqProd : deqSet -> deqSet -> deqSet **) |
---|
| 117 | let deqProd a b = |
---|
| 118 | Obj.magic (eq_pairs a b) |
---|
| 119 | |
---|
| 120 | (** val eq_sum : |
---|
| 121 | deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **) |
---|
| 122 | let eq_sum a b p1 p2 = |
---|
| 123 | match p1 with |
---|
| 124 | | Types.Inl a1 -> |
---|
| 125 | (match p2 with |
---|
| 126 | | Types.Inl a2 -> eqb a a1 a2 |
---|
| 127 | | Types.Inr b2 -> Bool.False) |
---|
| 128 | | Types.Inr b1 -> |
---|
| 129 | (match p2 with |
---|
| 130 | | Types.Inl a2 -> Bool.False |
---|
| 131 | | Types.Inr b2 -> eqb b b1 b2) |
---|
| 132 | |
---|
| 133 | (** val deqSum : deqSet -> deqSet -> deqSet **) |
---|
| 134 | let deqSum a b = |
---|
| 135 | Obj.magic (eq_sum a b) |
---|
| 136 | |
---|
| 137 | (** val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool **) |
---|
| 138 | let eq_sigma a p1 p2 = |
---|
| 139 | let a1 = p1 in let a2 = p2 in eqb a a1 a2 |
---|
| 140 | |
---|
| 141 | (** val deqSig : deqSet -> deqSet **) |
---|
| 142 | let deqSig a = |
---|
| 143 | Obj.magic (eq_sigma a) |
---|
| 144 | |
---|