source: driver/extracted/z.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.0 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Positive
18
19type z =
20| OZ
21| Pos of Positive.pos
22| Neg of Positive.pos
23
24val z_rect_Type4 :
25  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
26
27val z_rect_Type5 :
28  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
29
30val z_rect_Type3 :
31  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
32
33val z_rect_Type2 :
34  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
35
36val z_rect_Type1 :
37  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
38
39val z_rect_Type0 :
40  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
41
42val z_inv_rect_Type4 :
43  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
44  'a1) -> 'a1
45
46val z_inv_rect_Type3 :
47  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
48  'a1) -> 'a1
49
50val z_inv_rect_Type2 :
51  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
52  'a1) -> 'a1
53
54val z_inv_rect_Type1 :
55  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
56  'a1) -> 'a1
57
58val z_inv_rect_Type0 :
59  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
60  'a1) -> 'a1
61
62val z_discr : z -> z -> __
63
64val z_of_nat : Nat.nat -> z
65
66val neg_Z_of_nat : Nat.nat -> z
67
68val abs : z -> Nat.nat
69
70val oZ_test : z -> Bool.bool
71
72val zsucc : z -> z
73
74val zpred : z -> z
75
76val eqZb : z -> z -> Bool.bool
77
78val z_compare : z -> z -> Positive.compare
79
80val zplus : z -> z -> z
81
82val zopp : z -> z
83
84val zminus : z -> z -> z
85
86val z_two_power_nat : Nat.nat -> z
87
88val z_two_power_pos : Positive.pos -> z
89
90val two_p : z -> z
91
92open Types
93
94val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum
95
96val zleb : z -> z -> Bool.bool
97
98val zltb : z -> z -> Bool.bool
99
100val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
101
102val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
103
104val z_times : z -> z -> z
105
106val zmax : z -> z -> z
107
Note: See TracBrowser for help on using the repository browser.