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

Extraction


I

Int
Interface
IntFacts


S

String



Constructor 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