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 (142 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 (21 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 (3 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)
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 (11 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 (1 entry)
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 (3 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 (8 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 (5 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 (6 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 (73 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

Appᶠ [definition, in Translations.tsl_param3]


C

combine' [definition, in Translations.tsl_fun]
consistency_preservation [lemma, in Translations.tsl_param3]


D

debug_term [definition, in Translations.tsl_param]
default_term [definition, in Translations.tsl_param]


E

emptyTC [definition, in Translations.translation_utils]
eq [inductive, in Translations.tsl_param3]
equiv [definition, in Translations.tsl_param3]
eq_decl [definition, in Translations.tsl_param3]
eq_refl [constructor, in Translations.tsl_param3]
eq2 [inductive, in Translations.tsl_param3]
eqᶠ [definition, in Translations.tsl_param3]
Error [constructor, in Translations.translation_utils]
existᴿ [constructor, in Translations.tsl_param3]
existᵀ [definition, in Translations.tsl_param3]
existᶠ [definition, in Translations.tsl_param3]


F

FALSE [definition, in Translations.tsl_param3]
false_decl [definition, in Translations.tsl_param3]
Falseᶠ [definition, in Translations.tsl_param3]
fst [projection, in Translations.tsl_fun]


H

HasTwoElFstComponentᵗ [definition, in Translations.tsl_param3]


I

Id1 [module, in Translations.tsl_param]
Id1.free_thm_my_id [definition, in Translations.tsl_param]
Id1.ID [definition, in Translations.tsl_param]
Id1.my_id [definition, in Translations.tsl_param]
Id1.param_ID_identity [lemma, in Translations.tsl_param]
Id1.toto [definition, in Translations.tsl_param]
Id2 [module, in Translations.tsl_param]
Id2.free_thm_myf [definition, in Translations.tsl_param]
Id2.ID [definition, in Translations.tsl_param]
Id2.myf [definition, in Translations.tsl_param]
Id2.param_ID_identity [lemma, in Translations.tsl_param]
ImplParam [definition, in Translations.tsl_param3]
ImplParam [definition, in Translations.tsl_param2]


L

Lamᶠ [definition, in Translations.tsl_param3]
lookup_tsl_table [definition, in Translations.translation_utils]
lookup_tsl_table' [definition, in Translations.tsl_fun]


M

mkTYPE [definition, in Translations.tsl_param3]
mk_sig [constructor, in Translations.sigma]
monad_exc [instance, in Translations.translation_utils]


N

NotEnoughFuel [constructor, in Translations.translation_utils]


P

pack [definition, in Translations.sigma]
pair [constructor, in Translations.tsl_fun]
pair [definition, in Translations.sigma]
pairTrue [definition, in Translations.tsl_fun]
param [instance, in Translations.tsl_param]
param2_correctness [library]
param3_correctness [library]
pouet [definition, in Translations.tsl_fun]
prod [record, in Translations.tsl_fun]
prod_ind [definition, in Translations.tsl_fun]
Prodᶠ [definition, in Translations.tsl_param3]
proj [definition, in Translations.sigma]
proj1 [definition, in Translations.tsl_fun]
proj1 [definition, in Translations.sigma]
proj2 [definition, in Translations.tsl_fun]
proj2 [definition, in Translations.sigma]


R

refl2 [constructor, in Translations.tsl_param3]
reflᶠ [definition, in Translations.tsl_param3]
refresh_universes [definition, in Translations.tsl_param3]
replace [definition, in Translations.tsl_fun]
replace [definition, in Translations.tsl_param2]
rev_type [definition, in Translations.tsl_param]


S

sigma [record, in Translations.sigma]
sigma [library]
sigma_decl [definition, in Translations.tsl_param3]
sigma_ind [definition, in Translations.sigma]
sigmaᴿ [inductive, in Translations.tsl_param3]
sigmaᵀ [definition, in Translations.tsl_param3]
sigmaᶠ [definition, in Translations.tsl_param3]
snd [projection, in Translations.tsl_fun]
Success [constructor, in Translations.translation_utils]


T

T [definition, in Translations.tsl_param]
timesBool [definition, in Translations.tsl_fun]
tImplement [definition, in Translations.translation_utils]
tm [definition, in Translations.tsl_param]
todo [axiom, in Translations.translation_utils]
Translation [record, in Translations.translation_utils]
TranslationNotFound [constructor, in Translations.translation_utils]
TranslationNotHandeled [constructor, in Translations.translation_utils]
translation_utils [library]
TslParam [definition, in Translations.tsl_param3]
TslParam [definition, in Translations.tsl_param2]
tsl_name [definition, in Translations.translation_utils]
tsl_ident [definition, in Translations.translation_utils]
tsl_ind [projection, in Translations.translation_utils]
tsl_ty [projection, in Translations.translation_utils]
tsl_tm [projection, in Translations.translation_utils]
tsl_id [projection, in Translations.translation_utils]
tsl_monad [instance, in Translations.translation_utils]
tsl_result [inductive, in Translations.translation_utils]
tsl_error [inductive, in Translations.translation_utils]
tsl_context [definition, in Translations.translation_utils]
tsl_table [definition, in Translations.translation_utils]
tsl_param [instance, in Translations.tsl_param3]
tsl_term [definition, in Translations.tsl_param3]
tsl_rec [definition, in Translations.tsl_param3]
tsl_mind_body [definition, in Translations.tsl_param]
tsl_rec1 [definition, in Translations.tsl_param]
tsl_rec1_app [definition, in Translations.tsl_param]
tsl_rec0 [definition, in Translations.tsl_param]
tsl_fun [instance, in Translations.tsl_fun]
tsl_mind_body [definition, in Translations.tsl_fun]
tsl_rec [definition, in Translations.tsl_fun]
tsl_param [instance, in Translations.tsl_param2]
tsl_mind_body [definition, in Translations.tsl_param2]
tsl_term [definition, in Translations.tsl_param2]
tsl_rec2 [definition, in Translations.tsl_param2]
tsl_rec1 [definition, in Translations.tsl_param2]
tsl_param3 [library]
tsl_param2 [library]
tsl_param [library]
tsl_fun [library]
tTranslate [definition, in Translations.translation_utils]
Ty [definition, in Translations.tsl_param3]
ty [definition, in Translations.tsl_param2]
TypingError [constructor, in Translations.translation_utils]


V

Vectors [module, in Translations.tsl_param]


other

_ .2 (prod_scope) [notation, in Translations.tsl_fun]
_ .1 (prod_scope) [notation, in Translations.tsl_fun]
( _ ; _ ) (prod_scope) [notation, in Translations.tsl_fun]
_ .2 (sigma_scope) [notation, in Translations.sigma]
_ .1 (sigma_scope) [notation, in Translations.sigma]
( _ ; _ ) (sigma_scope) [notation, in Translations.sigma]
_ × _ (type_scope) [notation, in Translations.tsl_fun]
_ × _ (type_scope) [notation, in Translations.sigma]
exists _ .. _ , _ (type_scope) [notation, in Translations.sigma]
{ _ : _ & _ } (type_scope) [notation, in Translations.sigma]
_ · _ [notation, in Translations.tsl_param3]
_ →ᶠ _ [notation, in Translations.tsl_param3]
_ <= _ [notation, in Translations.tsl_param]
El _ [notation, in Translations.tsl_param3]
El _ [notation, in Translations.tsl_param2]
tsl_ty_param [notation, in Translations.tsl_param3]
tsl_ty_param [notation, in Translations.tsl_param2]
TYPE [notation, in Translations.tsl_param3]
TYPE [notation, in Translations.tsl_param2]
Πᶠ _ .. _ , _ [notation, in Translations.tsl_param3]
λᶠ _ .. _ , _ [notation, in Translations.tsl_param3]
ΣE [definition, in Translations.tsl_param3]
π1 [projection, in Translations.sigma]
π2 [projection, in Translations.sigma]



Notation Index

other

_ .2 (prod_scope) [in Translations.tsl_fun]
_ .1 (prod_scope) [in Translations.tsl_fun]
( _ ; _ ) (prod_scope) [in Translations.tsl_fun]
_ .2 (sigma_scope) [in Translations.sigma]
_ .1 (sigma_scope) [in Translations.sigma]
( _ ; _ ) (sigma_scope) [in Translations.sigma]
_ × _ (type_scope) [in Translations.tsl_fun]
_ × _ (type_scope) [in Translations.sigma]
exists _ .. _ , _ (type_scope) [in Translations.sigma]
{ _ : _ & _ } (type_scope) [in Translations.sigma]
_ · _ [in Translations.tsl_param3]
_ →ᶠ _ [in Translations.tsl_param3]
_ <= _ [in Translations.tsl_param]
El _ [in Translations.tsl_param3]
El _ [in Translations.tsl_param2]
tsl_ty_param [in Translations.tsl_param3]
tsl_ty_param [in Translations.tsl_param2]
TYPE [in Translations.tsl_param3]
TYPE [in Translations.tsl_param2]
Πᶠ _ .. _ , _ [in Translations.tsl_param3]
λᶠ _ .. _ , _ [in Translations.tsl_param3]



Module Index

I

Id1 [in Translations.tsl_param]
Id2 [in Translations.tsl_param]


V

Vectors [in Translations.tsl_param]



Library Index

P

param2_correctness
param3_correctness


S

sigma


T

translation_utils
tsl_param3
tsl_param2
tsl_param
tsl_fun



Constructor Index

E

eq_refl [in Translations.tsl_param3]
Error [in Translations.translation_utils]
existᴿ [in Translations.tsl_param3]


M

mk_sig [in Translations.sigma]


N

NotEnoughFuel [in Translations.translation_utils]


P

pair [in Translations.tsl_fun]


R

refl2 [in Translations.tsl_param3]


S

Success [in Translations.translation_utils]


T

TranslationNotFound [in Translations.translation_utils]
TranslationNotHandeled [in Translations.translation_utils]
TypingError [in Translations.translation_utils]



Axiom Index

T

todo [in Translations.translation_utils]



Lemma Index

C

consistency_preservation [in Translations.tsl_param3]


I

Id1.param_ID_identity [in Translations.tsl_param]
Id2.param_ID_identity [in Translations.tsl_param]



Projection Index

F

fst [in Translations.tsl_fun]


S

snd [in Translations.tsl_fun]


T

tsl_ind [in Translations.translation_utils]
tsl_ty [in Translations.translation_utils]
tsl_tm [in Translations.translation_utils]
tsl_id [in Translations.translation_utils]


other

π1 [in Translations.sigma]
π2 [in Translations.sigma]



Inductive Index

E

eq [in Translations.tsl_param3]
eq2 [in Translations.tsl_param3]


S

sigmaᴿ [in Translations.tsl_param3]


T

tsl_result [in Translations.translation_utils]
tsl_error [in Translations.translation_utils]



Instance Index

M

monad_exc [in Translations.translation_utils]


P

param [in Translations.tsl_param]


T

tsl_monad [in Translations.translation_utils]
tsl_param [in Translations.tsl_param3]
tsl_fun [in Translations.tsl_fun]
tsl_param [in Translations.tsl_param2]



Definition Index

A

Appᶠ [in Translations.tsl_param3]


C

combine' [in Translations.tsl_fun]


D

debug_term [in Translations.tsl_param]
default_term [in Translations.tsl_param]


E

emptyTC [in Translations.translation_utils]
equiv [in Translations.tsl_param3]
eq_decl [in Translations.tsl_param3]
eqᶠ [in Translations.tsl_param3]
existᵀ [in Translations.tsl_param3]
existᶠ [in Translations.tsl_param3]


F

FALSE [in Translations.tsl_param3]
false_decl [in Translations.tsl_param3]
Falseᶠ [in Translations.tsl_param3]


H

HasTwoElFstComponentᵗ [in Translations.tsl_param3]


I

Id1.free_thm_my_id [in Translations.tsl_param]
Id1.ID [in Translations.tsl_param]
Id1.my_id [in Translations.tsl_param]
Id1.toto [in Translations.tsl_param]
Id2.free_thm_myf [in Translations.tsl_param]
Id2.ID [in Translations.tsl_param]
Id2.myf [in Translations.tsl_param]
ImplParam [in Translations.tsl_param3]
ImplParam [in Translations.tsl_param2]


L

Lamᶠ [in Translations.tsl_param3]
lookup_tsl_table [in Translations.translation_utils]
lookup_tsl_table' [in Translations.tsl_fun]


M

mkTYPE [in Translations.tsl_param3]


P

pack [in Translations.sigma]
pair [in Translations.sigma]
pairTrue [in Translations.tsl_fun]
pouet [in Translations.tsl_fun]
prod_ind [in Translations.tsl_fun]
Prodᶠ [in Translations.tsl_param3]
proj [in Translations.sigma]
proj1 [in Translations.tsl_fun]
proj1 [in Translations.sigma]
proj2 [in Translations.tsl_fun]
proj2 [in Translations.sigma]


R

reflᶠ [in Translations.tsl_param3]
refresh_universes [in Translations.tsl_param3]
replace [in Translations.tsl_fun]
replace [in Translations.tsl_param2]
rev_type [in Translations.tsl_param]


S

sigma_decl [in Translations.tsl_param3]
sigma_ind [in Translations.sigma]
sigmaᵀ [in Translations.tsl_param3]
sigmaᶠ [in Translations.tsl_param3]


T

T [in Translations.tsl_param]
timesBool [in Translations.tsl_fun]
tImplement [in Translations.translation_utils]
tm [in Translations.tsl_param]
TslParam [in Translations.tsl_param3]
TslParam [in Translations.tsl_param2]
tsl_name [in Translations.translation_utils]
tsl_ident [in Translations.translation_utils]
tsl_context [in Translations.translation_utils]
tsl_table [in Translations.translation_utils]
tsl_term [in Translations.tsl_param3]
tsl_rec [in Translations.tsl_param3]
tsl_mind_body [in Translations.tsl_param]
tsl_rec1 [in Translations.tsl_param]
tsl_rec1_app [in Translations.tsl_param]
tsl_rec0 [in Translations.tsl_param]
tsl_mind_body [in Translations.tsl_fun]
tsl_rec [in Translations.tsl_fun]
tsl_mind_body [in Translations.tsl_param2]
tsl_term [in Translations.tsl_param2]
tsl_rec2 [in Translations.tsl_param2]
tsl_rec1 [in Translations.tsl_param2]
tTranslate [in Translations.translation_utils]
Ty [in Translations.tsl_param3]
ty [in Translations.tsl_param2]


other

ΣE [in Translations.tsl_param3]



Record Index

P

prod [in Translations.tsl_fun]


S

sigma [in Translations.sigma]


T

Translation [in Translations.translation_utils]



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 (142 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 (21 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 (3 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)
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 (11 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 (1 entry)
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 (3 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 (8 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 (5 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 (6 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 (73 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