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 (158 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 (27 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 (14 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 (2 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 (8 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 (81 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]
Appᶠ [definition, in Translations.tsl_param]


C

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


E

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


F

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


H

HasTwoElFstComponentᵗ [definition, in Translations.tsl_param3]
HasTwoElFstComponentᵗ [definition, in Translations.tsl_param]


I

ImplParam [definition, in Translations.tsl_param3]
ImplParam [definition, in Translations.tsl_param]
ImplParam [definition, in Translations.tsl_param2]


L

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


M

mkTYPE [definition, in Translations.tsl_param3]
mkTYPE [definition, in Translations.tsl_param]
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]
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]
Prodᶠ [definition, in Translations.tsl_param]
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]
refl2 [constructor, in Translations.tsl_param]
reflᶠ [definition, in Translations.tsl_param3]
reflᶠ [definition, in Translations.tsl_param]
refresh_universes [definition, in Translations.tsl_param3]
refresh_universes [definition, in Translations.tsl_param]
replace [definition, in Translations.tsl_fun]
replace [definition, in Translations.tsl_param2]


S

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


T

timesBool [definition, in Translations.tsl_fun]
tImplement [definition, in Translations.translation_utils]
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_param]
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_param [instance, in Translations.tsl_param]
tsl_term [definition, in Translations.tsl_param]
tsl_rec [definition, in Translations.tsl_param]
tsl_fun [instance, in Translations.tsl_fun]
tsl_mind_decl [definition, in Translations.tsl_fun]
tsl_rec [definition, in Translations.tsl_fun]
tsl_param [instance, in Translations.tsl_param2]
tsl_mind_decl [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_param]
ty [definition, in Translations.tsl_param2]
TypingError [constructor, in Translations.translation_utils]


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]
_ →ᶠ _ [notation, in Translations.tsl_param]
El _ [notation, in Translations.tsl_param3]
El _ [notation, in Translations.tsl_param]
El _ [notation, in Translations.tsl_param2]
tsl_ty_param [notation, in Translations.tsl_param3]
tsl_ty_param [notation, in Translations.tsl_param]
tsl_ty_param [notation, in Translations.tsl_param2]
TYPE [notation, in Translations.tsl_param3]
TYPE [notation, in Translations.tsl_param]
TYPE [notation, in Translations.tsl_param2]
Πᶠ _ .. _ , _ [notation, in Translations.tsl_param3]
Πᶠ _ .. _ , _ [notation, in Translations.tsl_param]
λᶠ _ .. _ , _ [notation, in Translations.tsl_param3]
λᶠ _ .. _ , _ [notation, in Translations.tsl_param]
ΣE [definition, in Translations.tsl_param3]
ΣE [definition, in Translations.tsl_param]
π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]
_ →ᶠ _ [in Translations.tsl_param]
El _ [in Translations.tsl_param3]
El _ [in Translations.tsl_param]
El _ [in Translations.tsl_param2]
tsl_ty_param [in Translations.tsl_param3]
tsl_ty_param [in Translations.tsl_param]
tsl_ty_param [in Translations.tsl_param2]
TYPE [in Translations.tsl_param3]
TYPE [in Translations.tsl_param]
TYPE [in Translations.tsl_param2]
Πᶠ _ .. _ , _ [in Translations.tsl_param3]
Πᶠ _ .. _ , _ [in Translations.tsl_param]
λᶠ _ .. _ , _ [in Translations.tsl_param3]
λᶠ _ .. _ , _ [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]
eq_refl [in Translations.tsl_param]
Error [in Translations.translation_utils]
existᴿ [in Translations.tsl_param3]
existᴿ [in Translations.tsl_param]


M

mk_sig [in Translations.sigma]


N

NotEnoughFuel [in Translations.translation_utils]


P

pair [in Translations.tsl_fun]


R

refl2 [in Translations.tsl_param3]
refl2 [in Translations.tsl_param]


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]
consistency_preservation [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]
eq [in Translations.tsl_param]
eq2 [in Translations.tsl_param3]
eq2 [in Translations.tsl_param]


S

sigmaᴿ [in Translations.tsl_param3]
sigmaᴿ [in Translations.tsl_param]


T

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



Instance Index

M

monad_exc [in Translations.translation_utils]


T

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



Definition Index

A

Appᶠ [in Translations.tsl_param3]
Appᶠ [in Translations.tsl_param]


C

combine' [in Translations.tsl_fun]


E

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


F

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


H

HasTwoElFstComponentᵗ [in Translations.tsl_param3]
HasTwoElFstComponentᵗ [in Translations.tsl_param]


I

ImplParam [in Translations.tsl_param3]
ImplParam [in Translations.tsl_param]
ImplParam [in Translations.tsl_param2]


L

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


M

mkTYPE [in Translations.tsl_param3]
mkTYPE [in Translations.tsl_param]


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]
Prodᶠ [in Translations.tsl_param]
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]
reflᶠ [in Translations.tsl_param]
refresh_universes [in Translations.tsl_param3]
refresh_universes [in Translations.tsl_param]
replace [in Translations.tsl_fun]
replace [in Translations.tsl_param2]


S

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


T

timesBool [in Translations.tsl_fun]
tImplement [in Translations.translation_utils]
TslParam [in Translations.tsl_param3]
TslParam [in Translations.tsl_param]
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_term [in Translations.tsl_param]
tsl_rec [in Translations.tsl_param]
tsl_mind_decl [in Translations.tsl_fun]
tsl_rec [in Translations.tsl_fun]
tsl_mind_decl [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_param]
ty [in Translations.tsl_param2]


other

ΣE [in Translations.tsl_param3]
ΣE [in Translations.tsl_param]



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 (158 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 (27 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 (14 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 (2 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 (8 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 (81 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