]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/z.mli
Control and copyright added.
[pkg-cerco/acc-trusted.git] / extracted / z.mli
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