| 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
axiomsF
fintypeP
POPLMarkS
SysFWellscopedLemma 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) |