| 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 | (361 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 | (226 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 | (4 entries) |
| 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 | (8 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 | (17 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 | (5 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 | (4 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 | (3 entries) |
| 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) |
| Abbreviation 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 | (52 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 | (3 entries) |
Global Index
A
abs [definition, in CoqFFI.Data.Int]acc:45 [binder, in CoqFFI.Data.Seq]
append [definition, in CoqFFI.Data.Seq]
a:1 [binder, in CoqFFI.Data.Result]
a:1 [binder, in CoqFFI.Data.Seq]
a:10 [binder, in CoqFFI.Data.Result]
a:11 [binder, in CoqFFI.Data.Seq]
a:13 [binder, in CoqFFI.Data.Seq]
a:14 [binder, in CoqFFI.Data.Seq]
a:16 [binder, in CoqFFI.Data.Result]
a:16 [binder, in CoqFFI.Data.Seq]
a:19 [binder, in CoqFFI.Data.Seq]
a:20 [binder, in CoqFFI.Data.Result]
a:23 [binder, in CoqFFI.Data.Seq]
a:26 [binder, in CoqFFI.Data.Result]
a:28 [binder, in CoqFFI.Data.Seq]
a:3 [binder, in CoqFFI.Data.Result]
a:32 [binder, in CoqFFI.Data.Result]
a:32 [binder, in CoqFFI.Data.Seq]
a:37 [binder, in CoqFFI.Data.Seq]
a:39 [binder, in CoqFFI.Data.Result]
a:4 [binder, in CoqFFI.Interface]
a:42 [binder, in CoqFFI.Data.Seq]
a:43 [binder, in CoqFFI.Data.Result]
a:47 [binder, in CoqFFI.Data.Result]
a:5 [binder, in CoqFFI.Data.Result]
a:55 [binder, in CoqFFI.Data.Result]
a:63 [binder, in CoqFFI.Data.Result]
a:67 [binder, in CoqFFI.Data.Result]
a:71 [binder, in CoqFFI.Data.Result]
a:8 [binder, in CoqFFI.Data.Seq]
B
bind [definition, in CoqFFI.Data.Result]b:11 [binder, in CoqFFI.Data.Result]
b:21 [binder, in CoqFFI.Data.Result]
b:24 [binder, in CoqFFI.Data.Seq]
b:33 [binder, in CoqFFI.Data.Seq]
b:38 [binder, in CoqFFI.Data.Seq]
b:43 [binder, in CoqFFI.Data.Seq]
C
ca:57 [binder, in CoqFFI.Data.Result]ce:58 [binder, in CoqFFI.Data.Result]
compare [definition, in CoqFFI.Data.Result]
cons [definition, in CoqFFI.Data.Seq]
Cons [constructor, in CoqFFI.Data.Seq]
c:34 [binder, in CoqFFI.Data.Result]
D
default:8 [binder, in CoqFFI.Data.Result]E
empty [definition, in CoqFFI.Data.Seq]eqa:49 [binder, in CoqFFI.Data.Result]
eqe:50 [binder, in CoqFFI.Data.Result]
equal [definition, in CoqFFI.Data.Result]
Err [abbreviation, in CoqFFI.Data.Result]
error [definition, in CoqFFI.Data.Result]
Exn [record, in CoqFFI.Exn]
exn [axiom, in CoqFFI.Exn]
Exn [library]
ExnExtraction [module, in CoqFFI.Exn]
Extraction [library]
e':28 [binder, in CoqFFI.Data.Result]
e:12 [binder, in CoqFFI.Data.Result]
e:17 [binder, in CoqFFI.Data.Result]
e:2 [binder, in CoqFFI.Exn]
e:2 [binder, in CoqFFI.Data.Result]
e:22 [binder, in CoqFFI.Data.Result]
e:27 [binder, in CoqFFI.Data.Result]
e:33 [binder, in CoqFFI.Data.Result]
e:4 [binder, in CoqFFI.Data.Result]
e:40 [binder, in CoqFFI.Data.Result]
e:44 [binder, in CoqFFI.Data.Result]
e:48 [binder, in CoqFFI.Data.Result]
e:56 [binder, in CoqFFI.Data.Result]
e:6 [binder, in CoqFFI.Data.Result]
e:64 [binder, in CoqFFI.Data.Result]
e:68 [binder, in CoqFFI.Data.Result]
e:72 [binder, in CoqFFI.Data.Result]
F
filter [definition, in CoqFFI.Data.Seq]filter_map [definition, in CoqFFI.Data.Seq]
flat_map [definition, in CoqFFI.Data.Seq]
fold [definition, in CoqFFI.Data.Result]
fold_left [definition, in CoqFFI.Data.Seq]
f:14 [binder, in CoqFFI.Data.Result]
f:23 [binder, in CoqFFI.Data.Result]
f:25 [binder, in CoqFFI.Data.Seq]
f:29 [binder, in CoqFFI.Data.Result]
f:29 [binder, in CoqFFI.Data.Seq]
f:34 [binder, in CoqFFI.Data.Seq]
f:35 [binder, in CoqFFI.Data.Result]
f:39 [binder, in CoqFFI.Data.Seq]
f:44 [binder, in CoqFFI.Data.Seq]
G
g:36 [binder, in CoqFFI.Data.Result]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]
is_error [definition, in CoqFFI.Data.Result]
is_ok [definition, in CoqFFI.Data.Result]
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_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]
i63_mod [definition, in CoqFFI.Data.Int]
i63_eqb_eq [lemma, in CoqFFI.Data.Int]
i:1 [binder, in CoqFFI.Data.String]
i:1 [binder, in CoqFFI.Interface]
J
join [definition, in CoqFFI.Data.Result]L
list_byte_of_string [definition, in CoqFFI.Data.String]lt:106 [binder, in CoqFFI.Data.IntFacts]
M
map [definition, in CoqFFI.Data.Result]map [definition, in CoqFFI.Data.Seq]
map_error [definition, in CoqFFI.Data.Result]
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]
N
Nil [constructor, in CoqFFI.Data.Seq]node [inductive, in CoqFFI.Data.Seq]
O
of_exn [projection, in CoqFFI.Exn]of_Z [definition, in CoqFFI.Data.Int]
ok [definition, in CoqFFI.Data.Result]
Ok [abbreviation, in CoqFFI.Data.Result]
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]
R
Result [library]ResultExtraction [module, in CoqFFI.Data.Result]
ret [definition, in CoqFFI.Data.Seq]
rst:18 [binder, in CoqFFI.Data.Seq]
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]
Seq [constructor, in CoqFFI.Data.Seq]
Seq [library]
SeqExtraction [module, in CoqFFI.Data.Seq]
String [library]
string_of_list_byte_fmt [definition, in CoqFFI.Data.String]
s:12 [binder, in CoqFFI.Data.Seq]
s:9 [binder, in CoqFFI.Data.Seq]
T
t [inductive, in CoqFFI.Data.Seq]to_exn [projection, in CoqFFI.Exn]
to_seq [definition, in CoqFFI.Data.Result]
to_list [definition, in CoqFFI.Data.Result]
to_option [definition, in CoqFFI.Data.Result]
to_Z [definition, in CoqFFI.Data.Int]
U
unpack [definition, in CoqFFI.Data.Seq]unseq [definition, in CoqFFI.Data.Seq]
un_i63_bound [lemma, in CoqFFI.Data.IntFacts]
un_i63 [projection, in CoqFFI.Data.Int]
V
value [definition, in CoqFFI.Data.Result]X
xneg:89 [binder, in CoqFFI.Data.IntFacts]xpos:68 [binder, in CoqFFI.Data.IntFacts]
xpos:71 [binder, in CoqFFI.Data.IntFacts]
x0:6 [binder, in CoqFFI.Data.Seq]
x1:7 [binder, in CoqFFI.Data.Seq]
x:1 [binder, in CoqFFI.Data.IntFacts]
x:10 [binder, in CoqFFI.Data.IntFacts]
x:10 [binder, in CoqFFI.Data.Int]
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:13 [binder, in CoqFFI.Data.Result]
x:14 [binder, in CoqFFI.Data.Int]
x:15 [binder, in CoqFFI.Data.Seq]
x:16 [binder, in CoqFFI.Data.IntFacts]
x:16 [binder, in CoqFFI.Data.Int]
x:17 [binder, in CoqFFI.Data.Seq]
x:18 [binder, in CoqFFI.Data.Result]
x:18 [binder, in CoqFFI.Data.Int]
x:19 [binder, in CoqFFI.Data.IntFacts]
x:20 [binder, in CoqFFI.Data.Int]
x:20 [binder, in CoqFFI.Data.Seq]
x:22 [binder, in CoqFFI.Data.IntFacts]
x:23 [binder, in CoqFFI.Data.Int]
x:24 [binder, in CoqFFI.Data.Result]
x:25 [binder, in CoqFFI.Data.IntFacts]
x:25 [binder, in CoqFFI.Data.Int]
x:26 [binder, in CoqFFI.Data.IntFacts]
x:26 [binder, in CoqFFI.Data.Seq]
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.IntFacts]
x:30 [binder, in CoqFFI.Data.Result]
x:30 [binder, in CoqFFI.Data.Int]
x:30 [binder, in CoqFFI.Data.Seq]
x:32 [binder, in CoqFFI.Data.IntFacts]
x:32 [binder, in CoqFFI.Data.Int]
x:34 [binder, in CoqFFI.Data.IntFacts]
x:35 [binder, in CoqFFI.Data.Seq]
x:37 [binder, in CoqFFI.Data.IntFacts]
x:37 [binder, in CoqFFI.Data.Result]
x:4 [binder, in CoqFFI.Data.String]
x:40 [binder, in CoqFFI.Data.IntFacts]
x:40 [binder, in CoqFFI.Data.Seq]
x:41 [binder, in CoqFFI.Data.Result]
x:43 [binder, in CoqFFI.Data.IntFacts]
x:44 [binder, in CoqFFI.Data.IntFacts]
x:45 [binder, in CoqFFI.Data.Result]
x:46 [binder, in CoqFFI.Data.Seq]
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:51 [binder, in CoqFFI.Data.Result]
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:59 [binder, in CoqFFI.Data.Result]
x:6 [binder, in CoqFFI.Data.Int]
x:63 [binder, in CoqFFI.Data.IntFacts]
x:65 [binder, in CoqFFI.Data.Result]
x:67 [binder, in CoqFFI.Data.IntFacts]
x:69 [binder, in CoqFFI.Data.Result]
x:7 [binder, in CoqFFI.Data.IntFacts]
x:7 [binder, in CoqFFI.Data.Result]
x:7 [binder, in CoqFFI.Data.Int]
x:70 [binder, in CoqFFI.Data.IntFacts]
x:73 [binder, in CoqFFI.Data.IntFacts]
x:73 [binder, in CoqFFI.Data.Result]
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.IntFacts]
y:11 [binder, in CoqFFI.Data.Int]
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.IntFacts]
y:17 [binder, in CoqFFI.Data.Int]
y:19 [binder, in CoqFFI.Data.Int]
y:20 [binder, in CoqFFI.Data.IntFacts]
y:21 [binder, in CoqFFI.Data.Int]
y:21 [binder, in CoqFFI.Data.Seq]
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.IntFacts]
y:31 [binder, in CoqFFI.Data.Int]
y:33 [binder, in CoqFFI.Data.IntFacts]
y:33 [binder, in CoqFFI.Data.Int]
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:52 [binder, in CoqFFI.Data.Result]
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:60 [binder, in CoqFFI.Data.Result]
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.String]
_ =? _ [notation, in CoqFFI.Data.Int]
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.String]
_ =? _ [in CoqFFI.Data.Int]
Binder Index
A
acc:45 [in CoqFFI.Data.Seq]a:1 [in CoqFFI.Data.Result]
a:1 [in CoqFFI.Data.Seq]
a:10 [in CoqFFI.Data.Result]
a:11 [in CoqFFI.Data.Seq]
a:13 [in CoqFFI.Data.Seq]
a:14 [in CoqFFI.Data.Seq]
a:16 [in CoqFFI.Data.Result]
a:16 [in CoqFFI.Data.Seq]
a:19 [in CoqFFI.Data.Seq]
a:20 [in CoqFFI.Data.Result]
a:23 [in CoqFFI.Data.Seq]
a:26 [in CoqFFI.Data.Result]
a:28 [in CoqFFI.Data.Seq]
a:3 [in CoqFFI.Data.Result]
a:32 [in CoqFFI.Data.Result]
a:32 [in CoqFFI.Data.Seq]
a:37 [in CoqFFI.Data.Seq]
a:39 [in CoqFFI.Data.Result]
a:4 [in CoqFFI.Interface]
a:42 [in CoqFFI.Data.Seq]
a:43 [in CoqFFI.Data.Result]
a:47 [in CoqFFI.Data.Result]
a:5 [in CoqFFI.Data.Result]
a:55 [in CoqFFI.Data.Result]
a:63 [in CoqFFI.Data.Result]
a:67 [in CoqFFI.Data.Result]
a:71 [in CoqFFI.Data.Result]
a:8 [in CoqFFI.Data.Seq]
B
b:11 [in CoqFFI.Data.Result]b:21 [in CoqFFI.Data.Result]
b:24 [in CoqFFI.Data.Seq]
b:33 [in CoqFFI.Data.Seq]
b:38 [in CoqFFI.Data.Seq]
b:43 [in CoqFFI.Data.Seq]
C
ca:57 [in CoqFFI.Data.Result]ce:58 [in CoqFFI.Data.Result]
c:34 [in CoqFFI.Data.Result]
D
default:8 [in CoqFFI.Data.Result]E
eqa:49 [in CoqFFI.Data.Result]eqe:50 [in CoqFFI.Data.Result]
e':28 [in CoqFFI.Data.Result]
e:12 [in CoqFFI.Data.Result]
e:17 [in CoqFFI.Data.Result]
e:2 [in CoqFFI.Exn]
e:2 [in CoqFFI.Data.Result]
e:22 [in CoqFFI.Data.Result]
e:27 [in CoqFFI.Data.Result]
e:33 [in CoqFFI.Data.Result]
e:4 [in CoqFFI.Data.Result]
e:40 [in CoqFFI.Data.Result]
e:44 [in CoqFFI.Data.Result]
e:48 [in CoqFFI.Data.Result]
e:56 [in CoqFFI.Data.Result]
e:6 [in CoqFFI.Data.Result]
e:64 [in CoqFFI.Data.Result]
e:68 [in CoqFFI.Data.Result]
e:72 [in CoqFFI.Data.Result]
F
f:14 [in CoqFFI.Data.Result]f:23 [in CoqFFI.Data.Result]
f:25 [in CoqFFI.Data.Seq]
f:29 [in CoqFFI.Data.Result]
f:29 [in CoqFFI.Data.Seq]
f:34 [in CoqFFI.Data.Seq]
f:35 [in CoqFFI.Data.Result]
f:39 [in CoqFFI.Data.Seq]
f:44 [in CoqFFI.Data.Seq]
G
g:36 [in CoqFFI.Data.Result]I
i:1 [in CoqFFI.Data.String]i:1 [in CoqFFI.Interface]
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]
R
rst:18 [in CoqFFI.Data.Seq]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]
s:12 [in CoqFFI.Data.Seq]
s:9 [in CoqFFI.Data.Seq]
X
xneg:89 [in CoqFFI.Data.IntFacts]xpos:68 [in CoqFFI.Data.IntFacts]
xpos:71 [in CoqFFI.Data.IntFacts]
x0:6 [in CoqFFI.Data.Seq]
x1:7 [in CoqFFI.Data.Seq]
x:1 [in CoqFFI.Data.IntFacts]
x:10 [in CoqFFI.Data.IntFacts]
x:10 [in CoqFFI.Data.Int]
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:13 [in CoqFFI.Data.Result]
x:14 [in CoqFFI.Data.Int]
x:15 [in CoqFFI.Data.Seq]
x:16 [in CoqFFI.Data.IntFacts]
x:16 [in CoqFFI.Data.Int]
x:17 [in CoqFFI.Data.Seq]
x:18 [in CoqFFI.Data.Result]
x:18 [in CoqFFI.Data.Int]
x:19 [in CoqFFI.Data.IntFacts]
x:20 [in CoqFFI.Data.Int]
x:20 [in CoqFFI.Data.Seq]
x:22 [in CoqFFI.Data.IntFacts]
x:23 [in CoqFFI.Data.Int]
x:24 [in CoqFFI.Data.Result]
x:25 [in CoqFFI.Data.IntFacts]
x:25 [in CoqFFI.Data.Int]
x:26 [in CoqFFI.Data.IntFacts]
x:26 [in CoqFFI.Data.Seq]
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.IntFacts]
x:30 [in CoqFFI.Data.Result]
x:30 [in CoqFFI.Data.Int]
x:30 [in CoqFFI.Data.Seq]
x:32 [in CoqFFI.Data.IntFacts]
x:32 [in CoqFFI.Data.Int]
x:34 [in CoqFFI.Data.IntFacts]
x:35 [in CoqFFI.Data.Seq]
x:37 [in CoqFFI.Data.IntFacts]
x:37 [in CoqFFI.Data.Result]
x:4 [in CoqFFI.Data.String]
x:40 [in CoqFFI.Data.IntFacts]
x:40 [in CoqFFI.Data.Seq]
x:41 [in CoqFFI.Data.Result]
x:43 [in CoqFFI.Data.IntFacts]
x:44 [in CoqFFI.Data.IntFacts]
x:45 [in CoqFFI.Data.Result]
x:46 [in CoqFFI.Data.Seq]
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:51 [in CoqFFI.Data.Result]
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:59 [in CoqFFI.Data.Result]
x:6 [in CoqFFI.Data.Int]
x:63 [in CoqFFI.Data.IntFacts]
x:65 [in CoqFFI.Data.Result]
x:67 [in CoqFFI.Data.IntFacts]
x:69 [in CoqFFI.Data.Result]
x:7 [in CoqFFI.Data.IntFacts]
x:7 [in CoqFFI.Data.Result]
x:7 [in CoqFFI.Data.Int]
x:70 [in CoqFFI.Data.IntFacts]
x:73 [in CoqFFI.Data.IntFacts]
x:73 [in CoqFFI.Data.Result]
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.IntFacts]
y:11 [in CoqFFI.Data.Int]
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.IntFacts]
y:17 [in CoqFFI.Data.Int]
y:19 [in CoqFFI.Data.Int]
y:20 [in CoqFFI.Data.IntFacts]
y:21 [in CoqFFI.Data.Int]
y:21 [in CoqFFI.Data.Seq]
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.IntFacts]
y:31 [in CoqFFI.Data.Int]
y:33 [in CoqFFI.Data.IntFacts]
y:33 [in CoqFFI.Data.Int]
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:52 [in CoqFFI.Data.Result]
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:60 [in CoqFFI.Data.Result]
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
E
ExnExtraction [in CoqFFI.Exn]I
IntExtraction [in CoqFFI.Data.Int]R
ResultExtraction [in CoqFFI.Data.Result]S
SeqExtraction [in CoqFFI.Data.Seq]Library Index
E
ExnExtraction
I
IntInterface
IntFacts
R
ResultS
SeqString
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_mul_assoc [in CoqFFI.Data.IntFacts]
i63_eqb_eq [in CoqFFI.Data.Int]
U
un_i63_bound [in CoqFFI.Data.IntFacts]Axiom Index
E
exn [in CoqFFI.Exn]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]
Constructor Index
C
Cons [in CoqFFI.Data.Seq]I
inject [in CoqFFI.Interface]M
mk_i63 [in CoqFFI.Data.Int]N
Nil [in CoqFFI.Data.Seq]S
Seq [in CoqFFI.Data.Seq]Projection Index
I
inject [in CoqFFI.Interface]O
of_exn [in CoqFFI.Exn]T
to_exn [in CoqFFI.Exn]U
un_i63 [in CoqFFI.Data.Int]Inductive Index
I
Inject [in CoqFFI.Interface]N
node [in CoqFFI.Data.Seq]T
t [in CoqFFI.Data.Seq]Instance Index
I
i63_le_Reflexive [in CoqFFI.Data.IntFacts]i63_lt_Transitive [in CoqFFI.Data.IntFacts]
i63_le_Transitive [in CoqFFI.Data.IntFacts]
Abbreviation Index
E
Err [in CoqFFI.Data.Result]O
Ok [in CoqFFI.Data.Result]Definition Index
A
abs [in CoqFFI.Data.Int]append [in CoqFFI.Data.Seq]
B
bind [in CoqFFI.Data.Result]C
compare [in CoqFFI.Data.Result]cons [in CoqFFI.Data.Seq]
E
empty [in CoqFFI.Data.Seq]equal [in CoqFFI.Data.Result]
error [in CoqFFI.Data.Result]
F
filter [in CoqFFI.Data.Seq]filter_map [in CoqFFI.Data.Seq]
flat_map [in CoqFFI.Data.Seq]
fold [in CoqFFI.Data.Result]
fold_left [in CoqFFI.Data.Seq]
I
ibinop [in CoqFFI.Data.Int]is_error [in CoqFFI.Data.Result]
is_ok [in CoqFFI.Data.Result]
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]
J
join [in CoqFFI.Data.Result]L
list_byte_of_string [in CoqFFI.Data.String]M
map [in CoqFFI.Data.Result]map [in CoqFFI.Data.Seq]
map_error [in CoqFFI.Data.Result]
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]ok [in CoqFFI.Data.Result]
R
ret [in CoqFFI.Data.Seq]S
string_of_list_byte_fmt [in CoqFFI.Data.String]T
to_seq [in CoqFFI.Data.Result]to_list [in CoqFFI.Data.Result]
to_option [in CoqFFI.Data.Result]
to_Z [in CoqFFI.Data.Int]
U
unpack [in CoqFFI.Data.Seq]unseq [in CoqFFI.Data.Seq]
V
value [in CoqFFI.Data.Result]Record Index
E
Exn [in CoqFFI.Exn]I
Inject [in CoqFFI.Interface]i63 [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 | (361 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 | (226 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 | (4 entries) |
| 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 | (8 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 | (17 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 | (5 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 | (4 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 | (3 entries) |
| 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) |
| Abbreviation 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 | (52 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 | (3 entries) |
This page has been generated by coqdoc