Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (130 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 entries) |
Global Index
A
abs [definition, in CoqFFI.Data.Int]a:4 [binder, in CoqFFI.Interface]
E
Extraction [library]I
ibinop [definition, in CoqFFI.Data.Int]inject [projection, in CoqFFI.Interface]
Inject [record, in CoqFFI.Interface]
inject [constructor, in CoqFFI.Interface]
Inject [inductive, in CoqFFI.Interface]
Int [library]
Interface [library]
IntExtraction [module, in CoqFFI.Data.Int]
IntFacts [library]
int_max_int [axiom, in CoqFFI.Data.IntFacts]
i63 [record, in CoqFFI.Data.Int]
i63add [definition, in CoqFFI.Data.Int]
i63add_safe_lt_add [lemma, in CoqFFI.Data.IntFacts]
i63add_safe_pos [lemma, in CoqFFI.Data.IntFacts]
i63add_unwrap_neg [lemma, in CoqFFI.Data.IntFacts]
i63add_sub_cancel [axiom, in CoqFFI.Data.IntFacts]
i63add_unwrap [axiom, in CoqFFI.Data.IntFacts]
i63add_min_safe [axiom, in CoqFFI.Data.IntFacts]
i63add_safe_lt [lemma, in CoqFFI.Data.IntFacts]
i63add_safe_le [lemma, in CoqFFI.Data.IntFacts]
i63add_safe [definition, in CoqFFI.Data.IntFacts]
i63add_comm [lemma, in CoqFFI.Data.IntFacts]
i63add_assoc [lemma, in CoqFFI.Data.IntFacts]
i63add_neutral [lemma, in CoqFFI.Data.IntFacts]
i63div [definition, in CoqFFI.Data.Int]
i63eqb [definition, in CoqFFI.Data.Int]
i63eq_eqb_false_equiv [axiom, in CoqFFI.Data.IntFacts]
i63eq_eqb_true_equiv [axiom, in CoqFFI.Data.IntFacts]
i63le [definition, in CoqFFI.Data.Int]
i63leb [definition, in CoqFFI.Data.Int]
i63leb_false_ltb [lemma, in CoqFFI.Data.IntFacts]
i63le_lt_trans [lemma, in CoqFFI.Data.IntFacts]
i63le_leb_false_equiv [axiom, in CoqFFI.Data.IntFacts]
i63le_leb_true_equiv [axiom, in CoqFFI.Data.IntFacts]
i63le_min_int [axiom, in CoqFFI.Data.IntFacts]
i63le_max_int [axiom, in CoqFFI.Data.IntFacts]
i63lt [definition, in CoqFFI.Data.Int]
i63ltb [definition, in CoqFFI.Data.Int]
i63ltb_false_leb [lemma, in CoqFFI.Data.IntFacts]
i63lt_le_succ [lemma, in CoqFFI.Data.IntFacts]
i63lt_le_pred [lemma, in CoqFFI.Data.IntFacts]
i63lt_le [lemma, in CoqFFI.Data.IntFacts]
i63lt_le_trans [lemma, in CoqFFI.Data.IntFacts]
i63lt_ltb_false_equiv [axiom, in CoqFFI.Data.IntFacts]
i63lt_ltb_true_equiv [axiom, in CoqFFI.Data.IntFacts]
i63lxor [definition, in CoqFFI.Data.Int]
i63max [definition, in CoqFFI.Data.Int]
i63min [definition, in CoqFFI.Data.Int]
i63mul [definition, in CoqFFI.Data.Int]
i63mul_comm [lemma, in CoqFFI.Data.IntFacts]
i63mul_neutral [lemma, in CoqFFI.Data.IntFacts]
i63neg_lt_le [lemma, in CoqFFI.Data.IntFacts]
i63neg_le_lt [lemma, in CoqFFI.Data.IntFacts]
i63sub [definition, in CoqFFI.Data.Int]
i63sub_safe_pos [lemma, in CoqFFI.Data.IntFacts]
i63sub_add_cancel [axiom, in CoqFFI.Data.IntFacts]
i63sub_unwrap [axiom, in CoqFFI.Data.IntFacts]
i63sub_max_safe [axiom, in CoqFFI.Data.IntFacts]
i63sub_safe [definition, in CoqFFI.Data.IntFacts]
i63_mod [definition, in CoqFFI.Data.Int]
i63_eqb_eq [lemma, in CoqFFI.Data.Int]
i63_mul_assoc [lemma, in CoqFFI.Data.IntFacts]
i63_well_founded_lt [axiom, in CoqFFI.Data.IntFacts]
i63_le_Reflexive [instance, in CoqFFI.Data.IntFacts]
i63_lt_Transitive [instance, in CoqFFI.Data.IntFacts]
i63_le_Transitive [instance, in CoqFFI.Data.IntFacts]
i:1 [binder, in CoqFFI.Interface]
i:1 [binder, in CoqFFI.Data.String]
L
list_byte_of_string [definition, in CoqFFI.Data.String]lt:106 [binder, in CoqFFI.Data.IntFacts]
M
max_int:22 [binder, in CoqFFI.Data.Int]max_i63 [definition, in CoqFFI.Data.Int]
max_int [definition, in CoqFFI.Data.Int]
max_uint [definition, in CoqFFI.Data.Int]
min_i63 [definition, in CoqFFI.Data.Int]
min_int [definition, in CoqFFI.Data.Int]
mk_i63 [constructor, in CoqFFI.Data.Int]
m:2 [binder, in CoqFFI.Interface]
O
of_Z [definition, in CoqFFI.Data.Int]op:9 [binder, in CoqFFI.Data.Int]
P
p:1 [binder, in CoqFFI.Data.Int]p:2 [binder, in CoqFFI.Data.Int]
p:3 [binder, in CoqFFI.Data.Int]
S
safe1:104 [binder, in CoqFFI.Data.IntFacts]safe2:105 [binder, in CoqFFI.Data.IntFacts]
safe:61 [binder, in CoqFFI.Data.IntFacts]
safe:65 [binder, in CoqFFI.Data.IntFacts]
safe:94 [binder, in CoqFFI.Data.IntFacts]
String [library]
string_of_list_byte_fmt [definition, in CoqFFI.Data.String]
T
to_Z [definition, in CoqFFI.Data.Int]U
un_i63 [projection, in CoqFFI.Data.Int]un_i63_bound [lemma, in CoqFFI.Data.IntFacts]
X
xneg:89 [binder, in CoqFFI.Data.IntFacts]xpos:68 [binder, in CoqFFI.Data.IntFacts]
xpos:71 [binder, in CoqFFI.Data.IntFacts]
x:1 [binder, in CoqFFI.Data.IntFacts]
x:10 [binder, in CoqFFI.Data.Int]
x:10 [binder, in CoqFFI.Data.IntFacts]
x:101 [binder, in CoqFFI.Data.IntFacts]
x:107 [binder, in CoqFFI.Data.IntFacts]
x:109 [binder, in CoqFFI.Data.IntFacts]
x:12 [binder, in CoqFFI.Data.Int]
x:13 [binder, in CoqFFI.Data.IntFacts]
x:14 [binder, in CoqFFI.Data.Int]
x:16 [binder, in CoqFFI.Data.Int]
x:16 [binder, in CoqFFI.Data.IntFacts]
x:18 [binder, in CoqFFI.Data.Int]
x:19 [binder, in CoqFFI.Data.IntFacts]
x:20 [binder, in CoqFFI.Data.Int]
x:22 [binder, in CoqFFI.Data.IntFacts]
x:23 [binder, in CoqFFI.Data.Int]
x:25 [binder, in CoqFFI.Data.Int]
x:25 [binder, in CoqFFI.Data.IntFacts]
x:26 [binder, in CoqFFI.Data.IntFacts]
x:27 [binder, in CoqFFI.Data.Int]
x:28 [binder, in CoqFFI.Data.IntFacts]
x:29 [binder, in CoqFFI.Data.Int]
x:3 [binder, in CoqFFI.Data.IntFacts]
x:30 [binder, in CoqFFI.Data.Int]
x:30 [binder, in CoqFFI.Data.IntFacts]
x:32 [binder, in CoqFFI.Data.Int]
x:32 [binder, in CoqFFI.Data.IntFacts]
x:34 [binder, in CoqFFI.Data.IntFacts]
x:37 [binder, in CoqFFI.Data.IntFacts]
x:4 [binder, in CoqFFI.Data.String]
x:40 [binder, in CoqFFI.Data.IntFacts]
x:43 [binder, in CoqFFI.Data.IntFacts]
x:44 [binder, in CoqFFI.Data.IntFacts]
x:47 [binder, in CoqFFI.Data.IntFacts]
x:49 [binder, in CoqFFI.Data.IntFacts]
x:5 [binder, in CoqFFI.Data.IntFacts]
x:50 [binder, in CoqFFI.Data.IntFacts]
x:53 [binder, in CoqFFI.Data.IntFacts]
x:55 [binder, in CoqFFI.Data.IntFacts]
x:57 [binder, in CoqFFI.Data.IntFacts]
x:59 [binder, in CoqFFI.Data.IntFacts]
x:6 [binder, in CoqFFI.Data.Int]
x:63 [binder, in CoqFFI.Data.IntFacts]
x:67 [binder, in CoqFFI.Data.IntFacts]
x:7 [binder, in CoqFFI.Data.Int]
x:7 [binder, in CoqFFI.Data.IntFacts]
x:70 [binder, in CoqFFI.Data.IntFacts]
x:73 [binder, in CoqFFI.Data.IntFacts]
x:77 [binder, in CoqFFI.Data.IntFacts]
x:8 [binder, in CoqFFI.Data.Int]
x:81 [binder, in CoqFFI.Data.IntFacts]
x:84 [binder, in CoqFFI.Data.IntFacts]
x:87 [binder, in CoqFFI.Data.IntFacts]
x:91 [binder, in CoqFFI.Data.IntFacts]
x:97 [binder, in CoqFFI.Data.IntFacts]
Y
ymax:100 [binder, in CoqFFI.Data.IntFacts]ymax:96 [binder, in CoqFFI.Data.IntFacts]
ymin:95 [binder, in CoqFFI.Data.IntFacts]
ymin:99 [binder, in CoqFFI.Data.IntFacts]
ypos:62 [binder, in CoqFFI.Data.IntFacts]
ypos:66 [binder, in CoqFFI.Data.IntFacts]
ypos:75 [binder, in CoqFFI.Data.IntFacts]
ypos:79 [binder, in CoqFFI.Data.IntFacts]
ypos:90 [binder, in CoqFFI.Data.IntFacts]
y:102 [binder, in CoqFFI.Data.IntFacts]
y:108 [binder, in CoqFFI.Data.IntFacts]
y:11 [binder, in CoqFFI.Data.Int]
y:11 [binder, in CoqFFI.Data.IntFacts]
y:110 [binder, in CoqFFI.Data.IntFacts]
y:13 [binder, in CoqFFI.Data.Int]
y:14 [binder, in CoqFFI.Data.IntFacts]
y:15 [binder, in CoqFFI.Data.Int]
y:17 [binder, in CoqFFI.Data.Int]
y:17 [binder, in CoqFFI.Data.IntFacts]
y:19 [binder, in CoqFFI.Data.Int]
y:20 [binder, in CoqFFI.Data.IntFacts]
y:21 [binder, in CoqFFI.Data.Int]
y:23 [binder, in CoqFFI.Data.IntFacts]
y:24 [binder, in CoqFFI.Data.Int]
y:26 [binder, in CoqFFI.Data.Int]
y:27 [binder, in CoqFFI.Data.IntFacts]
y:28 [binder, in CoqFFI.Data.Int]
y:29 [binder, in CoqFFI.Data.IntFacts]
y:31 [binder, in CoqFFI.Data.Int]
y:31 [binder, in CoqFFI.Data.IntFacts]
y:33 [binder, in CoqFFI.Data.Int]
y:33 [binder, in CoqFFI.Data.IntFacts]
y:35 [binder, in CoqFFI.Data.IntFacts]
y:38 [binder, in CoqFFI.Data.IntFacts]
y:41 [binder, in CoqFFI.Data.IntFacts]
y:45 [binder, in CoqFFI.Data.IntFacts]
y:48 [binder, in CoqFFI.Data.IntFacts]
y:51 [binder, in CoqFFI.Data.IntFacts]
y:54 [binder, in CoqFFI.Data.IntFacts]
y:56 [binder, in CoqFFI.Data.IntFacts]
y:58 [binder, in CoqFFI.Data.IntFacts]
y:60 [binder, in CoqFFI.Data.IntFacts]
y:64 [binder, in CoqFFI.Data.IntFacts]
y:74 [binder, in CoqFFI.Data.IntFacts]
y:78 [binder, in CoqFFI.Data.IntFacts]
y:8 [binder, in CoqFFI.Data.IntFacts]
y:82 [binder, in CoqFFI.Data.IntFacts]
y:85 [binder, in CoqFFI.Data.IntFacts]
y:88 [binder, in CoqFFI.Data.IntFacts]
y:92 [binder, in CoqFFI.Data.IntFacts]
y:98 [binder, in CoqFFI.Data.IntFacts]
Z
z:103 [binder, in CoqFFI.Data.IntFacts]z:36 [binder, in CoqFFI.Data.IntFacts]
z:39 [binder, in CoqFFI.Data.IntFacts]
z:46 [binder, in CoqFFI.Data.IntFacts]
z:52 [binder, in CoqFFI.Data.IntFacts]
z:93 [binder, in CoqFFI.Data.IntFacts]
other
_ mod _ (i63_scope) [notation, in CoqFFI.Data.Int]_ <=? _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ <? _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ <= _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ < _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ / _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ * _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ - _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ + _ (i63_scope) [notation, in CoqFFI.Data.Int]
_ =? _ [notation, in CoqFFI.Data.Int]
_ <$> _ [notation, in CoqFFI.Data.String]
Notation Index
other
_ mod _ (i63_scope) [in CoqFFI.Data.Int]_ <=? _ (i63_scope) [in CoqFFI.Data.Int]
_ <? _ (i63_scope) [in CoqFFI.Data.Int]
_ <= _ (i63_scope) [in CoqFFI.Data.Int]
_ < _ (i63_scope) [in CoqFFI.Data.Int]
_ / _ (i63_scope) [in CoqFFI.Data.Int]
_ * _ (i63_scope) [in CoqFFI.Data.Int]
_ - _ (i63_scope) [in CoqFFI.Data.Int]
_ + _ (i63_scope) [in CoqFFI.Data.Int]
_ =? _ [in CoqFFI.Data.Int]
_ <$> _ [in CoqFFI.Data.String]
Binder Index
A
a:4 [in CoqFFI.Interface]I
i:1 [in CoqFFI.Interface]i:1 [in CoqFFI.Data.String]
L
lt:106 [in CoqFFI.Data.IntFacts]M
max_int:22 [in CoqFFI.Data.Int]m:2 [in CoqFFI.Interface]
O
op:9 [in CoqFFI.Data.Int]P
p:1 [in CoqFFI.Data.Int]p:2 [in CoqFFI.Data.Int]
p:3 [in CoqFFI.Data.Int]
S
safe1:104 [in CoqFFI.Data.IntFacts]safe2:105 [in CoqFFI.Data.IntFacts]
safe:61 [in CoqFFI.Data.IntFacts]
safe:65 [in CoqFFI.Data.IntFacts]
safe:94 [in CoqFFI.Data.IntFacts]
X
xneg:89 [in CoqFFI.Data.IntFacts]xpos:68 [in CoqFFI.Data.IntFacts]
xpos:71 [in CoqFFI.Data.IntFacts]
x:1 [in CoqFFI.Data.IntFacts]
x:10 [in CoqFFI.Data.Int]
x:10 [in CoqFFI.Data.IntFacts]
x:101 [in CoqFFI.Data.IntFacts]
x:107 [in CoqFFI.Data.IntFacts]
x:109 [in CoqFFI.Data.IntFacts]
x:12 [in CoqFFI.Data.Int]
x:13 [in CoqFFI.Data.IntFacts]
x:14 [in CoqFFI.Data.Int]
x:16 [in CoqFFI.Data.Int]
x:16 [in CoqFFI.Data.IntFacts]
x:18 [in CoqFFI.Data.Int]
x:19 [in CoqFFI.Data.IntFacts]
x:20 [in CoqFFI.Data.Int]
x:22 [in CoqFFI.Data.IntFacts]
x:23 [in CoqFFI.Data.Int]
x:25 [in CoqFFI.Data.Int]
x:25 [in CoqFFI.Data.IntFacts]
x:26 [in CoqFFI.Data.IntFacts]
x:27 [in CoqFFI.Data.Int]
x:28 [in CoqFFI.Data.IntFacts]
x:29 [in CoqFFI.Data.Int]
x:3 [in CoqFFI.Data.IntFacts]
x:30 [in CoqFFI.Data.Int]
x:30 [in CoqFFI.Data.IntFacts]
x:32 [in CoqFFI.Data.Int]
x:32 [in CoqFFI.Data.IntFacts]
x:34 [in CoqFFI.Data.IntFacts]
x:37 [in CoqFFI.Data.IntFacts]
x:4 [in CoqFFI.Data.String]
x:40 [in CoqFFI.Data.IntFacts]
x:43 [in CoqFFI.Data.IntFacts]
x:44 [in CoqFFI.Data.IntFacts]
x:47 [in CoqFFI.Data.IntFacts]
x:49 [in CoqFFI.Data.IntFacts]
x:5 [in CoqFFI.Data.IntFacts]
x:50 [in CoqFFI.Data.IntFacts]
x:53 [in CoqFFI.Data.IntFacts]
x:55 [in CoqFFI.Data.IntFacts]
x:57 [in CoqFFI.Data.IntFacts]
x:59 [in CoqFFI.Data.IntFacts]
x:6 [in CoqFFI.Data.Int]
x:63 [in CoqFFI.Data.IntFacts]
x:67 [in CoqFFI.Data.IntFacts]
x:7 [in CoqFFI.Data.Int]
x:7 [in CoqFFI.Data.IntFacts]
x:70 [in CoqFFI.Data.IntFacts]
x:73 [in CoqFFI.Data.IntFacts]
x:77 [in CoqFFI.Data.IntFacts]
x:8 [in CoqFFI.Data.Int]
x:81 [in CoqFFI.Data.IntFacts]
x:84 [in CoqFFI.Data.IntFacts]
x:87 [in CoqFFI.Data.IntFacts]
x:91 [in CoqFFI.Data.IntFacts]
x:97 [in CoqFFI.Data.IntFacts]
Y
ymax:100 [in CoqFFI.Data.IntFacts]ymax:96 [in CoqFFI.Data.IntFacts]
ymin:95 [in CoqFFI.Data.IntFacts]
ymin:99 [in CoqFFI.Data.IntFacts]
ypos:62 [in CoqFFI.Data.IntFacts]
ypos:66 [in CoqFFI.Data.IntFacts]
ypos:75 [in CoqFFI.Data.IntFacts]
ypos:79 [in CoqFFI.Data.IntFacts]
ypos:90 [in CoqFFI.Data.IntFacts]
y:102 [in CoqFFI.Data.IntFacts]
y:108 [in CoqFFI.Data.IntFacts]
y:11 [in CoqFFI.Data.Int]
y:11 [in CoqFFI.Data.IntFacts]
y:110 [in CoqFFI.Data.IntFacts]
y:13 [in CoqFFI.Data.Int]
y:14 [in CoqFFI.Data.IntFacts]
y:15 [in CoqFFI.Data.Int]
y:17 [in CoqFFI.Data.Int]
y:17 [in CoqFFI.Data.IntFacts]
y:19 [in CoqFFI.Data.Int]
y:20 [in CoqFFI.Data.IntFacts]
y:21 [in CoqFFI.Data.Int]
y:23 [in CoqFFI.Data.IntFacts]
y:24 [in CoqFFI.Data.Int]
y:26 [in CoqFFI.Data.Int]
y:27 [in CoqFFI.Data.IntFacts]
y:28 [in CoqFFI.Data.Int]
y:29 [in CoqFFI.Data.IntFacts]
y:31 [in CoqFFI.Data.Int]
y:31 [in CoqFFI.Data.IntFacts]
y:33 [in CoqFFI.Data.Int]
y:33 [in CoqFFI.Data.IntFacts]
y:35 [in CoqFFI.Data.IntFacts]
y:38 [in CoqFFI.Data.IntFacts]
y:41 [in CoqFFI.Data.IntFacts]
y:45 [in CoqFFI.Data.IntFacts]
y:48 [in CoqFFI.Data.IntFacts]
y:51 [in CoqFFI.Data.IntFacts]
y:54 [in CoqFFI.Data.IntFacts]
y:56 [in CoqFFI.Data.IntFacts]
y:58 [in CoqFFI.Data.IntFacts]
y:60 [in CoqFFI.Data.IntFacts]
y:64 [in CoqFFI.Data.IntFacts]
y:74 [in CoqFFI.Data.IntFacts]
y:78 [in CoqFFI.Data.IntFacts]
y:8 [in CoqFFI.Data.IntFacts]
y:82 [in CoqFFI.Data.IntFacts]
y:85 [in CoqFFI.Data.IntFacts]
y:88 [in CoqFFI.Data.IntFacts]
y:92 [in CoqFFI.Data.IntFacts]
y:98 [in CoqFFI.Data.IntFacts]
Z
z:103 [in CoqFFI.Data.IntFacts]z:36 [in CoqFFI.Data.IntFacts]
z:39 [in CoqFFI.Data.IntFacts]
z:46 [in CoqFFI.Data.IntFacts]
z:52 [in CoqFFI.Data.IntFacts]
z:93 [in CoqFFI.Data.IntFacts]
Module Index
I
IntExtraction [in CoqFFI.Data.Int]Library Index
E
ExtractionI
IntInterface
IntFacts
S
StringConstructor Index
I
inject [in CoqFFI.Interface]M
mk_i63 [in CoqFFI.Data.Int]Lemma Index
I
i63add_safe_lt_add [in CoqFFI.Data.IntFacts]i63add_safe_pos [in CoqFFI.Data.IntFacts]
i63add_unwrap_neg [in CoqFFI.Data.IntFacts]
i63add_safe_lt [in CoqFFI.Data.IntFacts]
i63add_safe_le [in CoqFFI.Data.IntFacts]
i63add_comm [in CoqFFI.Data.IntFacts]
i63add_assoc [in CoqFFI.Data.IntFacts]
i63add_neutral [in CoqFFI.Data.IntFacts]
i63leb_false_ltb [in CoqFFI.Data.IntFacts]
i63le_lt_trans [in CoqFFI.Data.IntFacts]
i63ltb_false_leb [in CoqFFI.Data.IntFacts]
i63lt_le_succ [in CoqFFI.Data.IntFacts]
i63lt_le_pred [in CoqFFI.Data.IntFacts]
i63lt_le [in CoqFFI.Data.IntFacts]
i63lt_le_trans [in CoqFFI.Data.IntFacts]
i63mul_comm [in CoqFFI.Data.IntFacts]
i63mul_neutral [in CoqFFI.Data.IntFacts]
i63neg_lt_le [in CoqFFI.Data.IntFacts]
i63neg_le_lt [in CoqFFI.Data.IntFacts]
i63sub_safe_pos [in CoqFFI.Data.IntFacts]
i63_eqb_eq [in CoqFFI.Data.Int]
i63_mul_assoc [in CoqFFI.Data.IntFacts]
U
un_i63_bound [in CoqFFI.Data.IntFacts]Axiom Index
I
int_max_int [in CoqFFI.Data.IntFacts]i63add_sub_cancel [in CoqFFI.Data.IntFacts]
i63add_unwrap [in CoqFFI.Data.IntFacts]
i63add_min_safe [in CoqFFI.Data.IntFacts]
i63eq_eqb_false_equiv [in CoqFFI.Data.IntFacts]
i63eq_eqb_true_equiv [in CoqFFI.Data.IntFacts]
i63le_leb_false_equiv [in CoqFFI.Data.IntFacts]
i63le_leb_true_equiv [in CoqFFI.Data.IntFacts]
i63le_min_int [in CoqFFI.Data.IntFacts]
i63le_max_int [in CoqFFI.Data.IntFacts]
i63lt_ltb_false_equiv [in CoqFFI.Data.IntFacts]
i63lt_ltb_true_equiv [in CoqFFI.Data.IntFacts]
i63sub_add_cancel [in CoqFFI.Data.IntFacts]
i63sub_unwrap [in CoqFFI.Data.IntFacts]
i63sub_max_safe [in CoqFFI.Data.IntFacts]
i63_well_founded_lt [in CoqFFI.Data.IntFacts]
Projection Index
I
inject [in CoqFFI.Interface]U
un_i63 [in CoqFFI.Data.Int]Inductive Index
I
Inject [in CoqFFI.Interface]Instance Index
I
i63_le_Reflexive [in CoqFFI.Data.IntFacts]i63_lt_Transitive [in CoqFFI.Data.IntFacts]
i63_le_Transitive [in CoqFFI.Data.IntFacts]
Record Index
I
Inject [in CoqFFI.Interface]i63 [in CoqFFI.Data.Int]
Definition Index
A
abs [in CoqFFI.Data.Int]I
ibinop [in CoqFFI.Data.Int]i63add [in CoqFFI.Data.Int]
i63add_safe [in CoqFFI.Data.IntFacts]
i63div [in CoqFFI.Data.Int]
i63eqb [in CoqFFI.Data.Int]
i63le [in CoqFFI.Data.Int]
i63leb [in CoqFFI.Data.Int]
i63lt [in CoqFFI.Data.Int]
i63ltb [in CoqFFI.Data.Int]
i63lxor [in CoqFFI.Data.Int]
i63max [in CoqFFI.Data.Int]
i63min [in CoqFFI.Data.Int]
i63mul [in CoqFFI.Data.Int]
i63sub [in CoqFFI.Data.Int]
i63sub_safe [in CoqFFI.Data.IntFacts]
i63_mod [in CoqFFI.Data.Int]
L
list_byte_of_string [in CoqFFI.Data.String]M
max_i63 [in CoqFFI.Data.Int]max_int [in CoqFFI.Data.Int]
max_uint [in CoqFFI.Data.Int]
min_i63 [in CoqFFI.Data.Int]
min_int [in CoqFFI.Data.Int]
O
of_Z [in CoqFFI.Data.Int]S
string_of_list_byte_fmt [in CoqFFI.Data.String]T
to_Z [in CoqFFI.Data.Int]Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (130 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 entries) |
This page has been generated by coqdoc