| 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 | (115 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 | (4 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 | (9 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 | (21 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 | (50 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 | (9 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 | (22 entries) |
Global Index
A
anti_rename [lemma, in PR.sn_inductive_2a]app [constructor, in PR.stlc]
at_ty [definition, in PR.contexts]
B
Base [constructor, in PR.contexts]base [library]
C
closed_appR [lemma, in PR.sn_inductive_soundness_1a]closed_lam [lemma, in PR.sn_inductive_soundness_1a]
comp_idl [lemma, in PR.stlc]
comp_rinst_inst [lemma, in PR.stlc]
contexts [library]
cr [lemma, in PR.sn_inductive_2b]
ctx [definition, in PR.contexts]
E
env [definition, in PR.contexts]ext_SN [lemma, in PR.sn_inductive_2a]
F
Fun [constructor, in PR.contexts]fundamental_backwards [lemma, in PR.sn_inductive_soundness_1a]
I
idren [definition, in PR.contexts]ids [definition, in PR.stlc]
id_red [lemma, in PR.sn_inductive_2b]
ImPred [definition, in PR.reduction]
im_predI [lemma, in PR.reduction]
inst [definition, in PR.stlc]
inst_up_beta [lemma, in PR.stlc]
inst_idsE [lemma, in PR.stlc]
inst_comp [lemma, in PR.stlc]
inst_rinst_comp [lemma, in PR.stlc]
inst_ids [lemma, in PR.stlc]
L
lam [constructor, in PR.stlc]M
main_lemma [lemma, in PR.sn_inductive_2b]mstep [inductive, in PR.reduction]
mstep_beta [lemma, in PR.reduction]
mstep_subst [lemma, in PR.reduction]
mstep_inst [lemma, in PR.reduction]
mstep_app [lemma, in PR.reduction]
mstep_lam [lemma, in PR.reduction]
mstep_trans [lemma, in PR.reduction]
mstep_step [constructor, in PR.reduction]
mstep_refl [constructor, in PR.reduction]
N
neutral [definition, in PR.sn_inductive_soundness_1a]neutral_preservation [lemma, in PR.sn_inductive_soundness_1a]
norm [lemma, in PR.sn_inductive_2b]
P
pext [lemma, in PR.base]pi [lemma, in PR.base]
R
Red [definition, in PR.sn_inductive_2b]RedS [definition, in PR.sn_inductive_2b]
redsn [inductive, in PR.sn_inductive_soundness_1a]
redSN_ind_2 [definition, in PR.sn_defs]
redsn_backwards [lemma, in PR.sn_inductive_soundness_1a]
redsn_app [constructor, in PR.sn_inductive_soundness_1a]
redsn_beta [constructor, in PR.sn_inductive_soundness_1a]
reduction [library]
red_var [lemma, in PR.sn_inductive_2b]
ren [definition, in PR.contexts]
rename [lemma, in PR.sn_inductive_2a]
rename_redS [lemma, in PR.sn_inductive_2b]
rename_red [lemma, in PR.sn_inductive_2b]
rinst [definition, in PR.stlc]
rinst_idrenE [lemma, in PR.stlc]
rinst_inst_comp [lemma, in PR.stlc]
rinst_comp [lemma, in PR.stlc]
rinst_inst [lemma, in PR.stlc]
rinst_idren [lemma, in PR.stlc]
S
SAbs [constructor, in PR.sn_defs]SApp [constructor, in PR.sn_defs]
SAppl [constructor, in PR.sn_defs]
SBeta [constructor, in PR.sn_defs]
scomp [definition, in PR.contexts]
scons [definition, in PR.contexts]
sconsS [lemma, in PR.stlc]
scons_comp [lemma, in PR.contexts]
scons_eta_id [lemma, in PR.contexts]
scons_eta [lemma, in PR.contexts]
shift [definition, in PR.contexts]
SN [inductive, in PR.sn_defs]
sn [inductive, in PR.sn_defs]
SNe [inductive, in PR.sn_defs]
SNeu [constructor, in PR.sn_defs]
SNe_ind_2 [definition, in PR.sn_defs]
snI [constructor, in PR.sn_defs]
SNRed [inductive, in PR.sn_defs]
SN_multind [definition, in PR.sn_defs]
SN_ind_2 [definition, in PR.sn_defs]
sn_mstep [lemma, in PR.sn_defs]
SN_sn [lemma, in PR.sn_inductive_soundness_1b]
sn_app_neutral [lemma, in PR.sn_inductive_soundness_1a]
sn_confluence [lemma, in PR.sn_inductive_soundness_1a]
sn_inst [lemma, in PR.sn_inductive_soundness_1a]
sn_appL [lemma, in PR.sn_inductive_soundness_1a]
sn_preimage [lemma, in PR.sn_inductive_soundness_1a]
sn_inductive_soundness_1a [library]
sn_inductive_2a [library]
sn_inductive_soundness_1b [library]
sn_inductive_2b [library]
sn_defs [library]
SRed [constructor, in PR.sn_defs]
step [inductive, in PR.reduction]
step_inst [lemma, in PR.reduction]
step_weak [lemma, in PR.reduction]
step_appR [constructor, in PR.reduction]
step_appL [constructor, in PR.reduction]
step_abs [constructor, in PR.reduction]
step_beta [constructor, in PR.reduction]
stlc [library]
subst [definition, in PR.stlc]
SVar [constructor, in PR.sn_defs]
T
tm [inductive, in PR.stlc]ty [inductive, in PR.contexts]
U
up [definition, in PR.stlc]up_comp [lemma, in PR.stlc]
V
var [constructor, in PR.stlc]var0 [definition, in PR.contexts]
other
_ ∈ _ [notation, in PR.reduction]_ >> _ [notation, in PR.contexts]
_ .: _ [notation, in PR.contexts]
[ Pred _ | _ in _ ] [notation, in PR.reduction]
Notation Index
other
_ ∈ _ [in PR.reduction]_ >> _ [in PR.contexts]
_ .: _ [in PR.contexts]
[ Pred _ | _ in _ ] [in PR.reduction]
Library Index
B
baseC
contextsR
reductionS
sn_inductive_soundness_1asn_inductive_2a
sn_inductive_soundness_1b
sn_inductive_2b
sn_defs
stlc
Constructor Index
A
app [in PR.stlc]B
Base [in PR.contexts]F
Fun [in PR.contexts]L
lam [in PR.stlc]M
mstep_step [in PR.reduction]mstep_refl [in PR.reduction]
R
redsn_app [in PR.sn_inductive_soundness_1a]redsn_beta [in PR.sn_inductive_soundness_1a]
S
SAbs [in PR.sn_defs]SApp [in PR.sn_defs]
SAppl [in PR.sn_defs]
SBeta [in PR.sn_defs]
SNeu [in PR.sn_defs]
snI [in PR.sn_defs]
SRed [in PR.sn_defs]
step_appR [in PR.reduction]
step_appL [in PR.reduction]
step_abs [in PR.reduction]
step_beta [in PR.reduction]
SVar [in PR.sn_defs]
V
var [in PR.stlc]Lemma Index
A
anti_rename [in PR.sn_inductive_2a]C
closed_appR [in PR.sn_inductive_soundness_1a]closed_lam [in PR.sn_inductive_soundness_1a]
comp_idl [in PR.stlc]
comp_rinst_inst [in PR.stlc]
cr [in PR.sn_inductive_2b]
E
ext_SN [in PR.sn_inductive_2a]F
fundamental_backwards [in PR.sn_inductive_soundness_1a]I
id_red [in PR.sn_inductive_2b]im_predI [in PR.reduction]
inst_up_beta [in PR.stlc]
inst_idsE [in PR.stlc]
inst_comp [in PR.stlc]
inst_rinst_comp [in PR.stlc]
inst_ids [in PR.stlc]
M
main_lemma [in PR.sn_inductive_2b]mstep_beta [in PR.reduction]
mstep_subst [in PR.reduction]
mstep_inst [in PR.reduction]
mstep_app [in PR.reduction]
mstep_lam [in PR.reduction]
mstep_trans [in PR.reduction]
N
neutral_preservation [in PR.sn_inductive_soundness_1a]norm [in PR.sn_inductive_2b]
P
pext [in PR.base]pi [in PR.base]
R
redsn_backwards [in PR.sn_inductive_soundness_1a]red_var [in PR.sn_inductive_2b]
rename [in PR.sn_inductive_2a]
rename_redS [in PR.sn_inductive_2b]
rename_red [in PR.sn_inductive_2b]
rinst_idrenE [in PR.stlc]
rinst_inst_comp [in PR.stlc]
rinst_comp [in PR.stlc]
rinst_inst [in PR.stlc]
rinst_idren [in PR.stlc]
S
sconsS [in PR.stlc]scons_comp [in PR.contexts]
scons_eta_id [in PR.contexts]
scons_eta [in PR.contexts]
sn_mstep [in PR.sn_defs]
SN_sn [in PR.sn_inductive_soundness_1b]
sn_app_neutral [in PR.sn_inductive_soundness_1a]
sn_confluence [in PR.sn_inductive_soundness_1a]
sn_inst [in PR.sn_inductive_soundness_1a]
sn_appL [in PR.sn_inductive_soundness_1a]
sn_preimage [in PR.sn_inductive_soundness_1a]
step_inst [in PR.reduction]
step_weak [in PR.reduction]
U
up_comp [in PR.stlc]Inductive Index
M
mstep [in PR.reduction]R
redsn [in PR.sn_inductive_soundness_1a]S
SN [in PR.sn_defs]sn [in PR.sn_defs]
SNe [in PR.sn_defs]
SNRed [in PR.sn_defs]
step [in PR.reduction]
T
tm [in PR.stlc]ty [in PR.contexts]
Definition Index
A
at_ty [in PR.contexts]C
ctx [in PR.contexts]E
env [in PR.contexts]I
idren [in PR.contexts]ids [in PR.stlc]
ImPred [in PR.reduction]
inst [in PR.stlc]
N
neutral [in PR.sn_inductive_soundness_1a]R
Red [in PR.sn_inductive_2b]RedS [in PR.sn_inductive_2b]
redSN_ind_2 [in PR.sn_defs]
ren [in PR.contexts]
rinst [in PR.stlc]
S
scomp [in PR.contexts]scons [in PR.contexts]
shift [in PR.contexts]
SNe_ind_2 [in PR.sn_defs]
SN_multind [in PR.sn_defs]
SN_ind_2 [in PR.sn_defs]
subst [in PR.stlc]
U
up [in PR.stlc]V
var0 [in PR.contexts]| 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 | (115 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 | (4 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 | (9 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 | (21 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 | (50 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 | (9 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 | (22 entries) |