[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Bool |
---|
| 4 | |
---|
| 5 | open Relations |
---|
| 6 | |
---|
| 7 | open Nat |
---|
| 8 | |
---|
| 9 | open Hints_declaration |
---|
| 10 | |
---|
| 11 | open Core_notation |
---|
| 12 | |
---|
| 13 | open Pts |
---|
| 14 | |
---|
| 15 | open Logic |
---|
| 16 | |
---|
| 17 | open Positive |
---|
| 18 | |
---|
| 19 | type z = |
---|
| 20 | | OZ |
---|
| 21 | | Pos of Positive.pos |
---|
| 22 | | Neg of Positive.pos |
---|
| 23 | |
---|
| 24 | val z_rect_Type4 : |
---|
| 25 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 |
---|
| 26 | |
---|
| 27 | val z_rect_Type5 : |
---|
| 28 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 |
---|
| 29 | |
---|
| 30 | val z_rect_Type3 : |
---|
| 31 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 |
---|
| 32 | |
---|
| 33 | val z_rect_Type2 : |
---|
| 34 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 |
---|
| 35 | |
---|
| 36 | val z_rect_Type1 : |
---|
| 37 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 |
---|
| 38 | |
---|
| 39 | val z_rect_Type0 : |
---|
| 40 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 |
---|
| 41 | |
---|
| 42 | val z_inv_rect_Type4 : |
---|
| 43 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 44 | 'a1) -> 'a1 |
---|
| 45 | |
---|
| 46 | val z_inv_rect_Type3 : |
---|
| 47 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 48 | 'a1) -> 'a1 |
---|
| 49 | |
---|
| 50 | val z_inv_rect_Type2 : |
---|
| 51 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 52 | 'a1) -> 'a1 |
---|
| 53 | |
---|
| 54 | val z_inv_rect_Type1 : |
---|
| 55 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 56 | 'a1) -> 'a1 |
---|
| 57 | |
---|
| 58 | val z_inv_rect_Type0 : |
---|
| 59 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 60 | 'a1) -> 'a1 |
---|
| 61 | |
---|
| 62 | val z_discr : z -> z -> __ |
---|
| 63 | |
---|
| 64 | val z_of_nat : Nat.nat -> z |
---|
| 65 | |
---|
| 66 | val neg_Z_of_nat : Nat.nat -> z |
---|
| 67 | |
---|
| 68 | val abs : z -> Nat.nat |
---|
| 69 | |
---|
| 70 | val oZ_test : z -> Bool.bool |
---|
| 71 | |
---|
| 72 | val zsucc : z -> z |
---|
| 73 | |
---|
| 74 | val zpred : z -> z |
---|
| 75 | |
---|
| 76 | val eqZb : z -> z -> Bool.bool |
---|
| 77 | |
---|
| 78 | val z_compare : z -> z -> Positive.compare |
---|
| 79 | |
---|
| 80 | val zplus : z -> z -> z |
---|
| 81 | |
---|
| 82 | val zopp : z -> z |
---|
| 83 | |
---|
| 84 | val zminus : z -> z -> z |
---|
| 85 | |
---|
| 86 | val z_two_power_nat : Nat.nat -> z |
---|
| 87 | |
---|
| 88 | val z_two_power_pos : Positive.pos -> z |
---|
| 89 | |
---|
| 90 | val two_p : z -> z |
---|
| 91 | |
---|
| 92 | open Types |
---|
| 93 | |
---|
| 94 | val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum |
---|
| 95 | |
---|
| 96 | val zleb : z -> z -> Bool.bool |
---|
| 97 | |
---|
| 98 | val zltb : z -> z -> Bool.bool |
---|
| 99 | |
---|
| 100 | val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 |
---|
| 101 | |
---|
| 102 | val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 |
---|
| 103 | |
---|
| 104 | val z_times : z -> z -> z |
---|
| 105 | |
---|
| 106 | val zmax : z -> z -> z |
---|
| 107 | |
---|