[2601] | 1 | open Preamble |
---|

| 2 | |
---|

| 3 | open Types |
---|

| 4 | |
---|

| 5 | open Bool |
---|

| 6 | |
---|

| 7 | open Relations |
---|

| 8 | |
---|

| 9 | open Nat |
---|

| 10 | |
---|

| 11 | open Hints_declaration |
---|

| 12 | |
---|

| 13 | open Core_notation |
---|

| 14 | |
---|

| 15 | open Pts |
---|

| 16 | |
---|

| 17 | open Logic |
---|

| 18 | |
---|

| 19 | open Positive |
---|

| 20 | |
---|

| 21 | open Z |
---|

| 22 | |
---|

| 23 | type natp = |
---|

| 24 | | Pzero |
---|

| 25 | | Ppos of Positive.pos |
---|

| 26 | |
---|

| 27 | val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 |
---|

| 28 | |
---|

| 29 | val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 |
---|

| 30 | |
---|

| 31 | val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 |
---|

| 32 | |
---|

| 33 | val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 |
---|

| 34 | |
---|

| 35 | val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 |
---|

| 36 | |
---|

| 37 | val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 |
---|

| 38 | |
---|

| 39 | val natp_inv_rect_Type4 : |
---|

| 40 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 |
---|

| 41 | |
---|

| 42 | val natp_inv_rect_Type3 : |
---|

| 43 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 |
---|

| 44 | |
---|

| 45 | val natp_inv_rect_Type2 : |
---|

| 46 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 |
---|

| 47 | |
---|

| 48 | val natp_inv_rect_Type1 : |
---|

| 49 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 |
---|

| 50 | |
---|

| 51 | val natp_inv_rect_Type0 : |
---|

| 52 | natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 |
---|

| 53 | |
---|

| 54 | val natp_discr : natp -> natp -> __ |
---|

| 55 | |
---|

| 56 | val natp0 : natp -> natp |
---|

| 57 | |
---|

| 58 | val natp1 : natp -> natp |
---|

| 59 | |
---|

| 60 | val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod |
---|

| 61 | |
---|

| 62 | val div : Positive.pos -> Positive.pos -> natp |
---|

| 63 | |
---|

| 64 | val mod0 : Positive.pos -> Positive.pos -> natp |
---|

| 65 | |
---|

| 66 | val natp_plus : natp -> natp -> natp |
---|

| 67 | |
---|

| 68 | val natp_times : natp -> natp -> natp |
---|

| 69 | |
---|

| 70 | val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum |
---|

| 71 | |
---|

| 72 | val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum |
---|

| 73 | |
---|

| 74 | val natp_to_Z : natp -> Z.z |
---|

| 75 | |
---|

| 76 | val natp_to_negZ : natp -> Z.z |
---|

| 77 | |
---|

| 78 | val divZ : Z.z -> Z.z -> Z.z |
---|

| 79 | |
---|

| 80 | val modZ : Z.z -> Z.z -> Z.z |
---|

| 81 | |
---|