11 open Hints_declaration
25 | Ppos of Positive.pos
27 val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
29 val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
31 val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
33 val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
35 val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
37 val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
39 val natp_inv_rect_Type4 :
40 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
42 val natp_inv_rect_Type3 :
43 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
45 val natp_inv_rect_Type2 :
46 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
48 val natp_inv_rect_Type1 :
49 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
51 val natp_inv_rect_Type0 :
52 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
54 val natp_discr : natp -> natp -> __
56 val natp0 : natp -> natp
58 val natp1 : natp -> natp
60 val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod
62 val div : Positive.pos -> Positive.pos -> natp
64 val mod0 : Positive.pos -> Positive.pos -> natp
66 val natp_plus : natp -> natp -> natp
68 val natp_times : natp -> natp -> natp
70 val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum
72 val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum
74 val natp_to_Z : natp -> Z.z
76 val natp_to_negZ : natp -> Z.z
78 val divZ : Z.z -> Z.z -> Z.z
80 val modZ : Z.z -> Z.z -> Z.z