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 (256 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 (36 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 (4 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 (57 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 (39 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)
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 (17 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 (11 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 (11 entries)

Global Index

A

abs [constructor, in POPLMark.SysFWellscoped]
all [constructor, in POPLMark.SysFWellscoped]
ap [definition, in POPLMark.fintype]
apc [definition, in POPLMark.fintype]
app [constructor, in POPLMark.SysFWellscoped]
arr [constructor, in POPLMark.SysFWellscoped]
axioms [library]


C

can_form_all [lemma, in POPLMark.POPLMark]
can_form_arr [lemma, in POPLMark.POPLMark]
CommaNotation [module, in POPLMark.fintype]
_ , _ (subst_scope) [notation, in POPLMark.fintype]
comp [definition, in POPLMark.fintype]
compComp_tm [lemma, in POPLMark.SysFWellscoped]
compComp_ty [lemma, in POPLMark.SysFWellscoped]
compComp'_tm [lemma, in POPLMark.SysFWellscoped]
compComp'_ty [lemma, in POPLMark.SysFWellscoped]
compRenRen_tm [definition, in POPLMark.SysFWellscoped]
compRenRen_ty [definition, in POPLMark.SysFWellscoped]
compRenSubst_tm [definition, in POPLMark.SysFWellscoped]
compRenSubst_ty [definition, in POPLMark.SysFWellscoped]
compRen_tm [lemma, in POPLMark.SysFWellscoped]
compRen_ty [lemma, in POPLMark.SysFWellscoped]
compRen'_tm [lemma, in POPLMark.SysFWellscoped]
compRen'_ty [lemma, in POPLMark.SysFWellscoped]
compSubstRen__tm [definition, in POPLMark.SysFWellscoped]
compSubstRen__ty [definition, in POPLMark.SysFWellscoped]
compSubstSubst_tm [definition, in POPLMark.SysFWellscoped]
compSubstSubst_ty [definition, in POPLMark.SysFWellscoped]
congr_tabs [lemma, in POPLMark.SysFWellscoped]
congr_abs [lemma, in POPLMark.SysFWellscoped]
congr_vt [lemma, in POPLMark.SysFWellscoped]
congr_tapp [lemma, in POPLMark.SysFWellscoped]
congr_app [lemma, in POPLMark.SysFWellscoped]
congr_all [lemma, in POPLMark.SysFWellscoped]
congr_arr [lemma, in POPLMark.SysFWellscoped]
congr_top [lemma, in POPLMark.SysFWellscoped]
context_morphism_lemma [lemma, in POPLMark.POPLMark]
context_renaming_lemma [lemma, in POPLMark.POPLMark]
ctx [definition, in POPLMark.POPLMark]


D

dctx [definition, in POPLMark.POPLMark]


E

empty [definition, in POPLMark.POPLMark]
eval [inductive, in POPLMark.POPLMark]
ev_progress [lemma, in POPLMark.POPLMark]
extRen_tm [definition, in POPLMark.SysFWellscoped]
extRen_ty [definition, in POPLMark.SysFWellscoped]
ext_tm [definition, in POPLMark.SysFWellscoped]
ext_ty [definition, in POPLMark.SysFWellscoped]
E_TyFun [constructor, in POPLMark.POPLMark]
E_appArg [constructor, in POPLMark.POPLMark]
E_appFun [constructor, in POPLMark.POPLMark]
E_Tapptabs [constructor, in POPLMark.POPLMark]
E_appabs [constructor, in POPLMark.POPLMark]


F

fin [definition, in POPLMark.fintype]
fintype [library]
funcomp [definition, in POPLMark.fintype]


H

has_ty [inductive, in POPLMark.POPLMark]


I

id [definition, in POPLMark.fintype]
idren [definition, in POPLMark.fintype]
ids [projection, in POPLMark.fintype]
ids [constructor, in POPLMark.fintype]
idSubst_tm [definition, in POPLMark.SysFWellscoped]
idSubst_ty [definition, in POPLMark.SysFWellscoped]
instId_tm [lemma, in POPLMark.SysFWellscoped]
instId_ty [lemma, in POPLMark.SysFWellscoped]


N

null [definition, in POPLMark.fintype]


P

pext [axiom, in POPLMark.axioms]
pi [lemma, in POPLMark.axioms]
POPLMark [library]
preservation [lemma, in POPLMark.POPLMark]


R

ren [definition, in POPLMark.fintype]
renComp_tm [lemma, in POPLMark.SysFWellscoped]
renComp_ty [lemma, in POPLMark.SysFWellscoped]
renComp'_tm [lemma, in POPLMark.SysFWellscoped]
renComp'_ty [lemma, in POPLMark.SysFWellscoped]
renRen_tm [lemma, in POPLMark.SysFWellscoped]
renRen_ty [lemma, in POPLMark.SysFWellscoped]
renRen'_tm [lemma, in POPLMark.SysFWellscoped]
renRen'_ty [lemma, in POPLMark.SysFWellscoped]
Ren_tm [instance, in POPLMark.SysFWellscoped]
Ren_ty [instance, in POPLMark.SysFWellscoped]
ren_tm [definition, in POPLMark.SysFWellscoped]
ren_ty [definition, in POPLMark.SysFWellscoped]
ren1 [projection, in POPLMark.fintype]
Ren1 [record, in POPLMark.fintype]
ren1 [constructor, in POPLMark.fintype]
Ren1 [inductive, in POPLMark.fintype]
ren2 [projection, in POPLMark.fintype]
Ren2 [record, in POPLMark.fintype]
ren2 [constructor, in POPLMark.fintype]
Ren2 [inductive, in POPLMark.fintype]
ren3 [projection, in POPLMark.fintype]
Ren3 [record, in POPLMark.fintype]
ren3 [constructor, in POPLMark.fintype]
Ren3 [inductive, in POPLMark.fintype]
ren4 [projection, in POPLMark.fintype]
Ren4 [record, in POPLMark.fintype]
ren4 [constructor, in POPLMark.fintype]
Ren4 [inductive, in POPLMark.fintype]
ren5 [projection, in POPLMark.fintype]
Ren5 [record, in POPLMark.fintype]
ren5 [constructor, in POPLMark.fintype]
Ren5 [inductive, in POPLMark.fintype]
rinstId_tm [lemma, in POPLMark.SysFWellscoped]
rinstId_ty [lemma, in POPLMark.SysFWellscoped]
rinstInst_tm [lemma, in POPLMark.SysFWellscoped]
rinstInst_up_tm_tm [definition, in POPLMark.SysFWellscoped]
rinstInst_up_tm_ty [definition, in POPLMark.SysFWellscoped]
rinstInst_up_ty_tm [definition, in POPLMark.SysFWellscoped]
rinstInst_ty [lemma, in POPLMark.SysFWellscoped]
rinstInst_up_ty_ty [definition, in POPLMark.SysFWellscoped]
rinst_inst_tm [definition, in POPLMark.SysFWellscoped]
rinst_inst_ty [definition, in POPLMark.SysFWellscoped]


S

SA_all [constructor, in POPLMark.POPLMark]
SA_arrow [constructor, in POPLMark.POPLMark]
SA_Trans [constructor, in POPLMark.POPLMark]
SA_Refl [constructor, in POPLMark.POPLMark]
SA_top [constructor, in POPLMark.POPLMark]
scons [definition, in POPLMark.fintype]
scons_comp [lemma, in POPLMark.fintype]
scons_eta_id [lemma, in POPLMark.fintype]
scons_eta [lemma, in POPLMark.fintype]
shift [definition, in POPLMark.fintype]
sub [inductive, in POPLMark.POPLMark]
Subst_tm [instance, in POPLMark.SysFWellscoped]
Subst_ty [instance, in POPLMark.SysFWellscoped]
subst_tm [definition, in POPLMark.SysFWellscoped]
subst_ty [definition, in POPLMark.SysFWellscoped]
subst1 [projection, in POPLMark.fintype]
Subst1 [record, in POPLMark.fintype]
subst1 [constructor, in POPLMark.fintype]
Subst1 [inductive, in POPLMark.fintype]
subst2 [projection, in POPLMark.fintype]
Subst2 [record, in POPLMark.fintype]
subst2 [constructor, in POPLMark.fintype]
Subst2 [inductive, in POPLMark.fintype]
subst3 [projection, in POPLMark.fintype]
Subst3 [record, in POPLMark.fintype]
subst3 [constructor, in POPLMark.fintype]
Subst3 [inductive, in POPLMark.fintype]
subst4 [projection, in POPLMark.fintype]
Subst4 [record, in POPLMark.fintype]
subst4 [constructor, in POPLMark.fintype]
Subst4 [inductive, in POPLMark.fintype]
subst5 [projection, in POPLMark.fintype]
Subst5 [record, in POPLMark.fintype]
subst5 [constructor, in POPLMark.fintype]
Subst5 [inductive, in POPLMark.fintype]
sub_substitution [lemma, in POPLMark.POPLMark]
sub_trans [lemma, in POPLMark.POPLMark]
sub_trans' [lemma, in POPLMark.POPLMark]
sub_narrow [lemma, in POPLMark.POPLMark]
sub_weak1 [lemma, in POPLMark.POPLMark]
sub_weak [lemma, in POPLMark.POPLMark]
sub_refl [lemma, in POPLMark.POPLMark]
SysFWellscoped [library]


T

tabs [constructor, in POPLMark.SysFWellscoped]
tapp [constructor, in POPLMark.SysFWellscoped]
tm [inductive, in POPLMark.SysFWellscoped]
top [constructor, in POPLMark.SysFWellscoped]
transitivity_ren [lemma, in POPLMark.POPLMark]
transitivity_proj [lemma, in POPLMark.POPLMark]
transitivity_at [definition, in POPLMark.POPLMark]
ty [inductive, in POPLMark.SysFWellscoped]
ty_inv_tabs [lemma, in POPLMark.POPLMark]
ty_subst [lemma, in POPLMark.POPLMark]
ty_inv_abs [lemma, in POPLMark.POPLMark]
T_Sub [constructor, in POPLMark.POPLMark]
T_Tapp [constructor, in POPLMark.POPLMark]
T_tabs [constructor, in POPLMark.POPLMark]
T_app [constructor, in POPLMark.POPLMark]
T_abs [constructor, in POPLMark.POPLMark]
T_Var [constructor, in POPLMark.POPLMark]


U

upExtRen_tm_tm [definition, in POPLMark.SysFWellscoped]
upExtRen_tm_ty [definition, in POPLMark.SysFWellscoped]
upExtRen_ty_tm [definition, in POPLMark.SysFWellscoped]
upExtRen_ty_ty [definition, in POPLMark.SysFWellscoped]
upExt_tm_tm [definition, in POPLMark.SysFWellscoped]
upExt_tm_ty [definition, in POPLMark.SysFWellscoped]
upExt_ty_tm [definition, in POPLMark.SysFWellscoped]
upExt_ty_ty [definition, in POPLMark.SysFWellscoped]
upId_tm_tm [definition, in POPLMark.SysFWellscoped]
upId_tm_ty [definition, in POPLMark.SysFWellscoped]
upId_ty_tm [definition, in POPLMark.SysFWellscoped]
upId_ty_ty [definition, in POPLMark.SysFWellscoped]
upRen_tm_tm [definition, in POPLMark.SysFWellscoped]
upRen_tm_ty [definition, in POPLMark.SysFWellscoped]
upRen_ty_tm [definition, in POPLMark.SysFWellscoped]
upRen_ty_ty [definition, in POPLMark.SysFWellscoped]
up_subst_subst_tm_tm [definition, in POPLMark.SysFWellscoped]
up_subst_subst_tm_ty [definition, in POPLMark.SysFWellscoped]
up_subst_subst_ty_tm [definition, in POPLMark.SysFWellscoped]
up_subst_ren_tm_tm [definition, in POPLMark.SysFWellscoped]
up_subst_ren_tm_ty [definition, in POPLMark.SysFWellscoped]
up_subst_ren_ty_tm [definition, in POPLMark.SysFWellscoped]
up_ren_subst_tm_tm [definition, in POPLMark.SysFWellscoped]
up_ren_subst_tm_ty [definition, in POPLMark.SysFWellscoped]
up_ren_subst_ty_tm [definition, in POPLMark.SysFWellscoped]
up_tm_tm [definition, in POPLMark.SysFWellscoped]
up_tm_ty [definition, in POPLMark.SysFWellscoped]
up_ty_tm [definition, in POPLMark.SysFWellscoped]
up_subst_subst_ty_ty [definition, in POPLMark.SysFWellscoped]
up_subst_ren_ty_ty [definition, in POPLMark.SysFWellscoped]
up_ren_subst_ty_ty [definition, in POPLMark.SysFWellscoped]
up_ty_ty [definition, in POPLMark.SysFWellscoped]
up_ren_ren [lemma, in POPLMark.fintype]
up_ren [definition, in POPLMark.fintype]


V

value [inductive, in POPLMark.POPLMark]
Value_tabs [constructor, in POPLMark.POPLMark]
Value_abs [constructor, in POPLMark.POPLMark]
Var [record, in POPLMark.fintype]
Var [inductive, in POPLMark.fintype]
VarInstance_tm [instance, in POPLMark.SysFWellscoped]
VarInstance_ty [instance, in POPLMark.SysFWellscoped]
varLRen_tm [lemma, in POPLMark.SysFWellscoped]
varLRen_ty [lemma, in POPLMark.SysFWellscoped]
varL_tm [lemma, in POPLMark.SysFWellscoped]
varL_ty [lemma, in POPLMark.SysFWellscoped]
var_tm [constructor, in POPLMark.SysFWellscoped]
var_ty [constructor, in POPLMark.SysFWellscoped]
var_zero [definition, in POPLMark.fintype]
vt [constructor, in POPLMark.SysFWellscoped]


other

[ _ ; _ ] (fscope) [notation, in POPLMark.SysFWellscoped]
[ _ ] (fscope) [notation, in POPLMark.SysFWellscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in POPLMark.SysFWellscoped]
⟨ _ ⟩ (fscope) [notation, in POPLMark.SysFWellscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in POPLMark.fintype]
⟨ _ ⟩ (fscope) [notation, in POPLMark.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ [ _ ; _ ] (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ [ _ ] (subst_scope) [notation, in POPLMark.SysFWellscoped]
⇑__tm (subst_scope) [notation, in POPLMark.SysFWellscoped]
⇑__tm (subst_scope) [notation, in POPLMark.SysFWellscoped]
⇑__ty (subst_scope) [notation, in POPLMark.SysFWellscoped]
⇑__ty (subst_scope) [notation, in POPLMark.SysFWellscoped]
⇑__ty (subst_scope) [notation, in POPLMark.SysFWellscoped]
var (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ __tm (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ __tm (subst_scope) [notation, in POPLMark.SysFWellscoped]
var (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ __ty (subst_scope) [notation, in POPLMark.SysFWellscoped]
_ __ty (subst_scope) [notation, in POPLMark.SysFWellscoped]
↑ (subst_scope) [notation, in POPLMark.fintype]
_ .. (subst_scope) [notation, in POPLMark.fintype]
_ .: _ (subst_scope) [notation, in POPLMark.fintype]
_ [ _ ; _ ] (subst_scope) [notation, in POPLMark.fintype]
_ [ _ ] (subst_scope) [notation, in POPLMark.fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in POPLMark.fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in POPLMark.fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in POPLMark.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in POPLMark.fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in POPLMark.fintype]
_ >> _ [notation, in POPLMark.fintype]
EV _ => _ [notation, in POPLMark.POPLMark]
SUB _ |- _ <: _ [notation, in POPLMark.POPLMark]
TY _ ; _ |- _ : _ [notation, in POPLMark.POPLMark]



Notation Index

C

_ , _ (subst_scope) [in POPLMark.fintype]


other

[ _ ; _ ] (fscope) [in POPLMark.SysFWellscoped]
[ _ ] (fscope) [in POPLMark.SysFWellscoped]
⟨ _ ; _ ⟩ (fscope) [in POPLMark.SysFWellscoped]
⟨ _ ⟩ (fscope) [in POPLMark.SysFWellscoped]
⟨ _ ; _ ⟩ (fscope) [in POPLMark.fintype]
⟨ _ ⟩ (fscope) [in POPLMark.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in POPLMark.SysFWellscoped]
_ [ _ ; _ ] (subst_scope) [in POPLMark.SysFWellscoped]
_ ⟨ _ ⟩ (subst_scope) [in POPLMark.SysFWellscoped]
_ [ _ ] (subst_scope) [in POPLMark.SysFWellscoped]
⇑__tm (subst_scope) [in POPLMark.SysFWellscoped]
⇑__tm (subst_scope) [in POPLMark.SysFWellscoped]
⇑__ty (subst_scope) [in POPLMark.SysFWellscoped]
⇑__ty (subst_scope) [in POPLMark.SysFWellscoped]
⇑__ty (subst_scope) [in POPLMark.SysFWellscoped]
var (subst_scope) [in POPLMark.SysFWellscoped]
_ __tm (subst_scope) [in POPLMark.SysFWellscoped]
_ __tm (subst_scope) [in POPLMark.SysFWellscoped]
var (subst_scope) [in POPLMark.SysFWellscoped]
_ __ty (subst_scope) [in POPLMark.SysFWellscoped]
_ __ty (subst_scope) [in POPLMark.SysFWellscoped]
↑ (subst_scope) [in POPLMark.fintype]
_ .. (subst_scope) [in POPLMark.fintype]
_ .: _ (subst_scope) [in POPLMark.fintype]
_ [ _ ; _ ] (subst_scope) [in POPLMark.fintype]
_ [ _ ] (subst_scope) [in POPLMark.fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in POPLMark.fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in POPLMark.fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in POPLMark.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in POPLMark.fintype]
_ ⟨ _ ⟩ (subst_scope) [in POPLMark.fintype]
_ >> _ [in POPLMark.fintype]
EV _ => _ [in POPLMark.POPLMark]
SUB _ |- _ <: _ [in POPLMark.POPLMark]
TY _ ; _ |- _ : _ [in POPLMark.POPLMark]



Module Index

C

CommaNotation [in POPLMark.fintype]



Library Index

A

axioms


F

fintype


P

POPLMark


S

SysFWellscoped



Lemma Index

C

can_form_all [in POPLMark.POPLMark]
can_form_arr [in POPLMark.POPLMark]
compComp_tm [in POPLMark.SysFWellscoped]
compComp_ty [in POPLMark.SysFWellscoped]
compComp'_tm [in POPLMark.SysFWellscoped]
compComp'_ty [in POPLMark.SysFWellscoped]
compRen_tm [in POPLMark.SysFWellscoped]
compRen_ty [in POPLMark.SysFWellscoped]
compRen'_tm [in POPLMark.SysFWellscoped]
compRen'_ty [in POPLMark.SysFWellscoped]
congr_tabs [in POPLMark.SysFWellscoped]
congr_abs [in POPLMark.SysFWellscoped]
congr_vt [in POPLMark.SysFWellscoped]
congr_tapp [in POPLMark.SysFWellscoped]
congr_app [in POPLMark.SysFWellscoped]
congr_all [in POPLMark.SysFWellscoped]
congr_arr [in POPLMark.SysFWellscoped]
congr_top [in POPLMark.SysFWellscoped]
context_morphism_lemma [in POPLMark.POPLMark]
context_renaming_lemma [in POPLMark.POPLMark]


E

ev_progress [in POPLMark.POPLMark]


I

instId_tm [in POPLMark.SysFWellscoped]
instId_ty [in POPLMark.SysFWellscoped]


P

pi [in POPLMark.axioms]
preservation [in POPLMark.POPLMark]


R

renComp_tm [in POPLMark.SysFWellscoped]
renComp_ty [in POPLMark.SysFWellscoped]
renComp'_tm [in POPLMark.SysFWellscoped]
renComp'_ty [in POPLMark.SysFWellscoped]
renRen_tm [in POPLMark.SysFWellscoped]
renRen_ty [in POPLMark.SysFWellscoped]
renRen'_tm [in POPLMark.SysFWellscoped]
renRen'_ty [in POPLMark.SysFWellscoped]
rinstId_tm [in POPLMark.SysFWellscoped]
rinstId_ty [in POPLMark.SysFWellscoped]
rinstInst_tm [in POPLMark.SysFWellscoped]
rinstInst_ty [in POPLMark.SysFWellscoped]


S

scons_comp [in POPLMark.fintype]
scons_eta_id [in POPLMark.fintype]
scons_eta [in POPLMark.fintype]
sub_substitution [in POPLMark.POPLMark]
sub_trans [in POPLMark.POPLMark]
sub_trans' [in POPLMark.POPLMark]
sub_narrow [in POPLMark.POPLMark]
sub_weak1 [in POPLMark.POPLMark]
sub_weak [in POPLMark.POPLMark]
sub_refl [in POPLMark.POPLMark]


T

transitivity_ren [in POPLMark.POPLMark]
transitivity_proj [in POPLMark.POPLMark]
ty_inv_tabs [in POPLMark.POPLMark]
ty_subst [in POPLMark.POPLMark]
ty_inv_abs [in POPLMark.POPLMark]


U

up_ren_ren [in POPLMark.fintype]


V

varLRen_tm [in POPLMark.SysFWellscoped]
varLRen_ty [in POPLMark.SysFWellscoped]
varL_tm [in POPLMark.SysFWellscoped]
varL_ty [in POPLMark.SysFWellscoped]



Constructor Index

A

abs [in POPLMark.SysFWellscoped]
all [in POPLMark.SysFWellscoped]
app [in POPLMark.SysFWellscoped]
arr [in POPLMark.SysFWellscoped]


E

E_TyFun [in POPLMark.POPLMark]
E_appArg [in POPLMark.POPLMark]
E_appFun [in POPLMark.POPLMark]
E_Tapptabs [in POPLMark.POPLMark]
E_appabs [in POPLMark.POPLMark]


I

ids [in POPLMark.fintype]


R

ren1 [in POPLMark.fintype]
ren2 [in POPLMark.fintype]
ren3 [in POPLMark.fintype]
ren4 [in POPLMark.fintype]
ren5 [in POPLMark.fintype]


S

SA_all [in POPLMark.POPLMark]
SA_arrow [in POPLMark.POPLMark]
SA_Trans [in POPLMark.POPLMark]
SA_Refl [in POPLMark.POPLMark]
SA_top [in POPLMark.POPLMark]
subst1 [in POPLMark.fintype]
subst2 [in POPLMark.fintype]
subst3 [in POPLMark.fintype]
subst4 [in POPLMark.fintype]
subst5 [in POPLMark.fintype]


T

tabs [in POPLMark.SysFWellscoped]
tapp [in POPLMark.SysFWellscoped]
top [in POPLMark.SysFWellscoped]
T_Sub [in POPLMark.POPLMark]
T_Tapp [in POPLMark.POPLMark]
T_tabs [in POPLMark.POPLMark]
T_app [in POPLMark.POPLMark]
T_abs [in POPLMark.POPLMark]
T_Var [in POPLMark.POPLMark]


V

Value_tabs [in POPLMark.POPLMark]
Value_abs [in POPLMark.POPLMark]
var_tm [in POPLMark.SysFWellscoped]
var_ty [in POPLMark.SysFWellscoped]
vt [in POPLMark.SysFWellscoped]



Axiom Index

P

pext [in POPLMark.axioms]



Inductive Index

E

eval [in POPLMark.POPLMark]


H

has_ty [in POPLMark.POPLMark]


R

Ren1 [in POPLMark.fintype]
Ren2 [in POPLMark.fintype]
Ren3 [in POPLMark.fintype]
Ren4 [in POPLMark.fintype]
Ren5 [in POPLMark.fintype]


S

sub [in POPLMark.POPLMark]
Subst1 [in POPLMark.fintype]
Subst2 [in POPLMark.fintype]
Subst3 [in POPLMark.fintype]
Subst4 [in POPLMark.fintype]
Subst5 [in POPLMark.fintype]


T

tm [in POPLMark.SysFWellscoped]
ty [in POPLMark.SysFWellscoped]


V

value [in POPLMark.POPLMark]
Var [in POPLMark.fintype]



Projection Index

I

ids [in POPLMark.fintype]


R

ren1 [in POPLMark.fintype]
ren2 [in POPLMark.fintype]
ren3 [in POPLMark.fintype]
ren4 [in POPLMark.fintype]
ren5 [in POPLMark.fintype]


S

subst1 [in POPLMark.fintype]
subst2 [in POPLMark.fintype]
subst3 [in POPLMark.fintype]
subst4 [in POPLMark.fintype]
subst5 [in POPLMark.fintype]



Instance Index

R

Ren_tm [in POPLMark.SysFWellscoped]
Ren_ty [in POPLMark.SysFWellscoped]


S

Subst_tm [in POPLMark.SysFWellscoped]
Subst_ty [in POPLMark.SysFWellscoped]


V

VarInstance_tm [in POPLMark.SysFWellscoped]
VarInstance_ty [in POPLMark.SysFWellscoped]



Definition Index

A

ap [in POPLMark.fintype]
apc [in POPLMark.fintype]


C

comp [in POPLMark.fintype]
compRenRen_tm [in POPLMark.SysFWellscoped]
compRenRen_ty [in POPLMark.SysFWellscoped]
compRenSubst_tm [in POPLMark.SysFWellscoped]
compRenSubst_ty [in POPLMark.SysFWellscoped]
compSubstRen__tm [in POPLMark.SysFWellscoped]
compSubstRen__ty [in POPLMark.SysFWellscoped]
compSubstSubst_tm [in POPLMark.SysFWellscoped]
compSubstSubst_ty [in POPLMark.SysFWellscoped]
ctx [in POPLMark.POPLMark]


D

dctx [in POPLMark.POPLMark]


E

empty [in POPLMark.POPLMark]
extRen_tm [in POPLMark.SysFWellscoped]
extRen_ty [in POPLMark.SysFWellscoped]
ext_tm [in POPLMark.SysFWellscoped]
ext_ty [in POPLMark.SysFWellscoped]


F

fin [in POPLMark.fintype]
funcomp [in POPLMark.fintype]


I

id [in POPLMark.fintype]
idren [in POPLMark.fintype]
idSubst_tm [in POPLMark.SysFWellscoped]
idSubst_ty [in POPLMark.SysFWellscoped]


N

null [in POPLMark.fintype]


R

ren [in POPLMark.fintype]
ren_tm [in POPLMark.SysFWellscoped]
ren_ty [in POPLMark.SysFWellscoped]
rinstInst_up_tm_tm [in POPLMark.SysFWellscoped]
rinstInst_up_tm_ty [in POPLMark.SysFWellscoped]
rinstInst_up_ty_tm [in POPLMark.SysFWellscoped]
rinstInst_up_ty_ty [in POPLMark.SysFWellscoped]
rinst_inst_tm [in POPLMark.SysFWellscoped]
rinst_inst_ty [in POPLMark.SysFWellscoped]


S

scons [in POPLMark.fintype]
shift [in POPLMark.fintype]
subst_tm [in POPLMark.SysFWellscoped]
subst_ty [in POPLMark.SysFWellscoped]


T

transitivity_at [in POPLMark.POPLMark]


U

upExtRen_tm_tm [in POPLMark.SysFWellscoped]
upExtRen_tm_ty [in POPLMark.SysFWellscoped]
upExtRen_ty_tm [in POPLMark.SysFWellscoped]
upExtRen_ty_ty [in POPLMark.SysFWellscoped]
upExt_tm_tm [in POPLMark.SysFWellscoped]
upExt_tm_ty [in POPLMark.SysFWellscoped]
upExt_ty_tm [in POPLMark.SysFWellscoped]
upExt_ty_ty [in POPLMark.SysFWellscoped]
upId_tm_tm [in POPLMark.SysFWellscoped]
upId_tm_ty [in POPLMark.SysFWellscoped]
upId_ty_tm [in POPLMark.SysFWellscoped]
upId_ty_ty [in POPLMark.SysFWellscoped]
upRen_tm_tm [in POPLMark.SysFWellscoped]
upRen_tm_ty [in POPLMark.SysFWellscoped]
upRen_ty_tm [in POPLMark.SysFWellscoped]
upRen_ty_ty [in POPLMark.SysFWellscoped]
up_subst_subst_tm_tm [in POPLMark.SysFWellscoped]
up_subst_subst_tm_ty [in POPLMark.SysFWellscoped]
up_subst_subst_ty_tm [in POPLMark.SysFWellscoped]
up_subst_ren_tm_tm [in POPLMark.SysFWellscoped]
up_subst_ren_tm_ty [in POPLMark.SysFWellscoped]
up_subst_ren_ty_tm [in POPLMark.SysFWellscoped]
up_ren_subst_tm_tm [in POPLMark.SysFWellscoped]
up_ren_subst_tm_ty [in POPLMark.SysFWellscoped]
up_ren_subst_ty_tm [in POPLMark.SysFWellscoped]
up_tm_tm [in POPLMark.SysFWellscoped]
up_tm_ty [in POPLMark.SysFWellscoped]
up_ty_tm [in POPLMark.SysFWellscoped]
up_subst_subst_ty_ty [in POPLMark.SysFWellscoped]
up_subst_ren_ty_ty [in POPLMark.SysFWellscoped]
up_ren_subst_ty_ty [in POPLMark.SysFWellscoped]
up_ty_ty [in POPLMark.SysFWellscoped]
up_ren [in POPLMark.fintype]


V

var_zero [in POPLMark.fintype]



Record Index

R

Ren1 [in POPLMark.fintype]
Ren2 [in POPLMark.fintype]
Ren3 [in POPLMark.fintype]
Ren4 [in POPLMark.fintype]
Ren5 [in POPLMark.fintype]


S

Subst1 [in POPLMark.fintype]
Subst2 [in POPLMark.fintype]
Subst3 [in POPLMark.fintype]
Subst4 [in POPLMark.fintype]
Subst5 [in POPLMark.fintype]


V

Var [in POPLMark.fintype]



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 (256 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 (36 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 (4 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 (57 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 (39 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)
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 (17 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 (11 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 (11 entries)