| 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 | (640 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 | (51 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 | (25 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 | (15 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 | (235 entries) |
| Section 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 | (13 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 | (103 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 | (44 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 | (42 entries) |
| Abbreviation 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) |
| 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 | (65 entries) |
| Variable 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) |
| 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 | (29 entries) |
Global Index
A
adequacy [definition, in Framework]adequacy_cadequacy [lemma, in Framework]
agree_equiv [lemma, in Freevars]
agree_ty [lemma, in Freevars]
annot [definition, in Autosubst_Basics]
app [inductive, in Filters]
App [constructor, in Definitions]
app [constructor, in CL1]
arr [constructor, in STLC1]
arr [constructor, in T1]
arr [constructor, in F1]
Arr [constructor, in Definitions]
arr [constructor, in CL1]
Autosubst [library]
Autosubst_MMapInstances [library]
Autosubst_Classes [library]
Autosubst_Derive [library]
Autosubst_MMap [library]
Autosubst_Tactics [library]
Autosubst_Basics [library]
Autosubst_Lemmas [library]
B
base [constructor, in STLC1]BASE [constructor, in Definitions]
base [constructor, in CL1]
basetype [inductive, in Definitions]
bot [definition, in Filters]
bot_filter [lemma, in Filters]
C
cadequacy [definition, in Framework]cequi_typep [instance, in Types]
cint [definition, in Definitions]
cint_csub_r [lemma, in Contexts]
cint_csub_l [lemma, in Contexts]
cint_Empty [lemma, in Contexts]
cint_Gamma_Empty [lemma, in Contexts]
cint_Empty_Gamma [lemma, in Contexts]
CL [inductive, in CL1]
CLapp [constructor, in CL1]
CLC [definition, in CL1]
CLC_c [lemma, in CL1]
CLK [constructor, in CL1]
closed_leu [projection, in Filters]
closed_int [projection, in Filters]
closure [inductive, in Filters]
closure_closure_equiv [lemma, in Filters]
closure_filter_equiv [lemma, in Filters]
closure_filter [lemma, in Filters]
CLS [constructor, in CL1]
CL_stlc [lemma, in CL1]
CL_valid [lemma, in CL1]
cl_step_appR [constructor, in CL1]
cl_step_appL [constructor, in CL1]
cl_stepK [constructor, in CL1]
cl_stepS [constructor, in CL1]
cl_step [inductive, in CL1]
CL_ty [inductive, in CL1]
CL1 [library]
compA [lemma, in Autosubst_Basics]
compatible [definition, in Interpretation]
compatible_sub [lemma, in Interpretation]
compatible_sub_Gamma [lemma, in Interpretation]
compatible_cint [lemma, in Interpretation]
compatible_down [lemma, in Interpretation]
compatible_up [lemma, in Interpretation]
compile [definition, in T1]
compiler_consistency [definition, in Framework]
compile_subst [lemma, in T1]
compile_subst_full [lemma, in T1]
compile_ren_full [lemma, in T1]
comp_id [lemma, in Autosubst_Basics]
conj' [lemma, in Autosubst_Basics]
cons_drop_inv [lemma, in Contexts]
context [definition, in Definitions]
Contexts [library]
count [definition, in TypeEquivalence]
csplit [lemma, in Contexts]
csub [definition, in Definitions]
csub_ext [lemma, in Contexts]
csub_cint_proper [instance, in Contexts]
csub_cint_comp [lemma, in Contexts]
csub_comm [lemma, in Contexts]
csub_sub [lemma, in Contexts]
cte [definition, in Definitions]
cte_eq [lemma, in Contexts]
cte_ext_int [lemma, in Contexts]
cte_ext [lemma, in Contexts]
cte_csub_R [lemma, in Contexts]
cte_csub_L [lemma, in Contexts]
cte_csub_equiv [lemma, in Contexts]
cte_csub [instance, in Contexts]
cte_cint_proper [instance, in Contexts]
cte_equivalence [instance, in Contexts]
cte_trans [lemma, in Contexts]
cte_sym [lemma, in Contexts]
cte_pwr_refl [lemma, in Contexts]
cte_refl [lemma, in Contexts]
cte_comp_cint [lemma, in Contexts]
cte_assoc_cint [lemma, in Contexts]
cte_comm_cint [lemma, in Contexts]
D
Dec [record, in Decidable]Dec [inductive, in Decidable]
dec [definition, in Decidable]
Decidable [library]
decide [projection, in Decidable]
decide [constructor, in Decidable]
decide_lt_nat [instance, in Decidable]
decide_le_nat [instance, in Decidable]
decide_eq_nat [instance, in Decidable]
Definitions [library]
drop [definition, in Definitions]
E
Empty [definition, in Definitions]equal_f [lemma, in Autosubst_Basics]
equiv_comp_p [instance, in Filters]
equiv_app_comp [lemma, in Filters]
equiv_filter [lemma, in Filters]
equiv_e [instance, in Filters]
equiv_closure [lemma, in Filters]
equiv_rp_p [instance, in RealizorPredicates]
equiv_closed [projection, in RealizorPredicates]
equi_typep [instance, in Types]
equi_type [lemma, in Types]
excl_bot [projection, in RealizorPredicates]
F
fapp [constructor, in F1]feq_eq [lemma, in Contexts]
feq_trans [lemma, in Contexts]
feq_ext_int [lemma, in Contexts]
feq_ext [lemma, in Contexts]
fgen [constructor, in F1]
Filters [library]
filter_filter_equiv [lemma, in Filters]
filter_equiv_trans [lemma, in Filters]
filter_equiv_sym [lemma, in Filters]
filter_equiv_refl [lemma, in Filters]
filter_equiv [definition, in Filters]
filter_ind_filter [lemma, in Filters]
flam [constructor, in F1]
fold_ren_cons [lemma, in Autosubst_Tactics]
Framework [library]
Freevars [library]
fromclosure_F [lemma, in Filters]
fspec [constructor, in F1]
Ftype [inductive, in F1]
funcomp [definition, in Autosubst_Basics]
FV [inductive, in Freevars]
FVAppL [constructor, in Freevars]
FVAppR [constructor, in Freevars]
fvar [constructor, in F1]
FVLam [constructor, in Freevars]
FVVar [constructor, in Freevars]
FV_dec [instance, in Freevars]
f_ty [inductive, in F1]
f_ctx [definition, in F1]
F1 [library]
F2 [library]
G
General_Termination.LambdaCurry.tty [variable, in Framework]General_Termination.LambdaCurry [section, in Framework]
General_Termination.Compiler.tstep [variable, in Framework]
General_Termination.Compiler.vtty [variable, in Framework]
General_Termination.Compiler.ctty [variable, in Framework]
[| _ |] [notation, in Framework]
General_Termination.Compiler.compiler [variable, in Framework]
General_Termination.Compiler.tterm [variable, in Framework]
General_Termination.Compiler [section, in Framework]
[[ _ ]] _ [notation, in Framework]
General_Termination.int_ty [variable, in Framework]
General_Termination.ttype [variable, in Framework]
General_Termination [section, in Framework]
gsn [constructor, in Reduction]
GSN [inductive, in Reduction]
H
hcomp [definition, in Autosubst_Classes]hcomp_dist_internal [lemma, in Autosubst_Derive]
hcomp_ren_internal [lemma, in Autosubst_Derive]
hcomp_lift_internal [lemma, in Autosubst_Derive]
hcomp_lift_n_internal [lemma, in Autosubst_Derive]
hsubst [projection, in Autosubst_Classes]
HSubst [record, in Autosubst_Classes]
hsubst [constructor, in Autosubst_Classes]
HSubst [inductive, in Autosubst_Classes]
HSubstHSubstComp [record, in Autosubst_Classes]
HSubstHSubstComp [inductive, in Autosubst_Classes]
HSubstHSubstInd [record, in Autosubst_Classes]
HSubstHSubstInd [inductive, in Autosubst_Classes]
HSubstLemmas [record, in Autosubst_Classes]
hsubst_hsubst_ind [projection, in Autosubst_Classes]
hsubst_hsubst_ind [constructor, in Autosubst_Classes]
hsubst_hsubst_comp [projection, in Autosubst_Classes]
hsubst_hsubst_comp [constructor, in Autosubst_Classes]
hsubst_comp [projection, in Autosubst_Classes]
hsubst_id [projection, in Autosubst_Classes]
hsubst_compR [lemma, in Autosubst_Tactics]
hsubst_compX [lemma, in Autosubst_Tactics]
hsubst_compI [lemma, in Autosubst_Tactics]
hsubst_idX [lemma, in Autosubst_Tactics]
I
id [definition, in Autosubst_Basics]ids [projection, in Autosubst_Classes]
Ids [record, in Autosubst_Classes]
ids [constructor, in Autosubst_Classes]
Ids [inductive, in Autosubst_Classes]
Ids_Tterm [instance, in T1]
Ids_ftype [instance, in F1]
Ids_term [instance, in Definitions]
id_hsubst [projection, in Autosubst_Classes]
id_subst [projection, in Autosubst_Classes]
id_hsubstR [lemma, in Autosubst_Tactics]
id_hsubstX [lemma, in Autosubst_Tactics]
id_scompR [lemma, in Autosubst_Tactics]
id_scompX [lemma, in Autosubst_Tactics]
id_comp [lemma, in Autosubst_Basics]
IFilter [record, in Filters]
inApp [constructor, in Filters]
inc [definition, in Weakening]
inclosure_F [lemma, in Filters]
includes [inductive, in Subsumption]
includesDropL [constructor, in Subsumption]
includesDropR [constructor, in Subsumption]
includesF [constructor, in Subsumption]
incl_inv_sub [lemma, in Subsumption]
incl_top [projection, in RealizorPredicates]
inF [constructor, in Filters]
inI [constructor, in Filters]
inKtype [constructor, in T1]
int [definition, in Definitions]
Int [constructor, in Definitions]
InternalLemmas [section, in Autosubst_Derive]
InternalLemmasHSubst [section, in Autosubst_Derive]
Interpretation [library]
intersect [definition, in RealizorPredicates]
intersect_realizable [lemma, in RealizorPredicates]
intty [constructor, in Interpretation]
inttype [inductive, in Definitions]
int_lam [lemma, in Premodel]
int_st [lemma, in Premodel]
int_x [lemma, in Premodel]
int_ty_rp [lemma, in STLC1]
int_ty [definition, in STLC1]
int_ty_rp [lemma, in T1]
int_ty [definition, in T1]
int_nat_filter [lemma, in T1]
int_nat [inductive, in T1]
int_ty_beta [lemma, in F1]
int_ty_subst_equiv [lemma, in F1]
int_ty_ren_equiv [lemma, in F1]
int_ty_feq_equiv [lemma, in F1]
int_ty_rp [lemma, in F1]
int_ty [definition, in F1]
int_app [definition, in Filters]
int_ty_rp [lemma, in CL1]
int_ty [definition, in CL1]
int_eq_O [lemma, in TypeEquivalence]
int_comm_O [lemma, in TypeEquivalence]
int_O [lemma, in TypeEquivalence]
int_equiv [instance, in RealizorPredicates]
int_IF [lemma, in Interpretation]
int_t [inductive, in Interpretation]
invtyInt [lemma, in Types]
invtyVar [lemma, in Types]
in_int_ty [lemma, in STLC1]
in_int_ty [lemma, in T1]
in_int_ty [lemma, in F1]
in_int_ty [lemma, in CL1]
iterate [definition, in Autosubst_Basics]
iterate_0 [lemma, in Autosubst_Basics]
iterate_S [lemma, in Autosubst_Basics]
iter_param [lemma, in Autosubst_Derive]
iter_fp [lemma, in Autosubst_Derive]
K
K [constructor, in CL1]Ktype [inductive, in T1]
k_nat [lemma, in T1]
L
Lam [constructor, in Definitions]lcc [definition, in Framework]
lcc_c [lemma, in Framework]
LemmasForFun [section, in Autosubst_Basics]
LemmasForHSubst [section, in Autosubst_Tactics]
LemmasForMMap [section, in Autosubst_MMap]
LemmasForSubst [section, in Autosubst_Tactics]
lift [definition, in Autosubst_Basics]
lift_injn [lemma, in Autosubst_Lemmas]
lift_inj [lemma, in Autosubst_Lemmas]
lift_eta [lemma, in Autosubst_Basics]
lift_compR [lemma, in Autosubst_Basics]
lift_comp [lemma, in Autosubst_Basics]
lift_scons [lemma, in Autosubst_Basics]
lift0 [lemma, in Autosubst_Lemmas]
lift0 [lemma, in Autosubst_Basics]
M
mmap [projection, in Autosubst_MMap]MMap [record, in Autosubst_MMap]
mmap [constructor, in Autosubst_MMap]
MMap [inductive, in Autosubst_MMap]
MMapConst [section, in Autosubst_MMap]
MMapExt [record, in Autosubst_MMap]
MMapExt [inductive, in Autosubst_MMap]
MMapExt_const [instance, in Autosubst_MMap]
MMapExt_refl [instance, in Autosubst_MMap]
MMapExt_fun [instance, in Autosubst_MMapInstances]
MMapExt_pair [instance, in Autosubst_MMapInstances]
MMapExt_list [instance, in Autosubst_MMapInstances]
MMapExt_option [instance, in Autosubst_MMapInstances]
MMapId [section, in Autosubst_MMap]
MMapInstances [section, in Autosubst_MMapInstances]
MMapInstances.A [variable, in Autosubst_MMapInstances]
MMapInstances.B [variable, in Autosubst_MMapInstances]
MMapInstances.C [variable, in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_C [variable, in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_B [variable, in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_C [variable, in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_B [variable, in Autosubst_MMapInstances]
MMapInstances.MMap_A_C [variable, in Autosubst_MMapInstances]
MMapInstances.MMap_A_B [variable, in Autosubst_MMapInstances]
MMapLemmas [record, in Autosubst_MMap]
MMapLemmas_const [instance, in Autosubst_MMap]
MMapLemmas_refl [instance, in Autosubst_MMap]
MMapLemmas_fun [instance, in Autosubst_MMapInstances]
MMapLemmas_pair [instance, in Autosubst_MMapInstances]
MMapLemmas_list [instance, in Autosubst_MMapInstances]
MMapLemmas_option [instance, in Autosubst_MMapInstances]
mmap_const_instE [lemma, in Autosubst_MMap]
MMap_const [instance, in Autosubst_MMap]
mmap_id_instE [lemma, in Autosubst_MMap]
MMap_refl [instance, in Autosubst_MMap]
mmap_compR [lemma, in Autosubst_MMap]
mmap_compX [lemma, in Autosubst_MMap]
mmap_idX [lemma, in Autosubst_MMap]
mmap_comp [projection, in Autosubst_MMap]
mmap_id [projection, in Autosubst_MMap]
mmap_ext [projection, in Autosubst_MMap]
mmap_ext [constructor, in Autosubst_MMap]
MMap_fun [instance, in Autosubst_MMapInstances]
MMap_pair [instance, in Autosubst_MMapInstances]
MMap_list [instance, in Autosubst_MMapInstances]
MMap_option [instance, in Autosubst_MMapInstances]
mmap_id_ext [lemma, in Autosubst_Derive]
more [constructor, in Reduction]
N
NAT [constructor, in T1]O
OMEGA [constructor, in Definitions]one [constructor, in Reduction]
only_filter [projection, in RealizorPredicates]
O_nat [constructor, in T1]
P
pi [constructor, in F1]pi_equiv [definition, in RealizorPredicates]
plusA [lemma, in Autosubst_Basics]
plusnO [lemma, in Autosubst_Basics]
plusnS [lemma, in Autosubst_Basics]
plusOn [lemma, in Autosubst_Basics]
plusSn [lemma, in Autosubst_Basics]
possible_int_specialize [lemma, in RealizorPredicates]
possible_int_realizable [lemma, in RealizorPredicates]
possible_int [definition, in RealizorPredicates]
Premodel [library]
prod [definition, in RealizorPredicates]
prod_equiv [instance, in RealizorPredicates]
prod_realizable [lemma, in RealizorPredicates]
PWR [definition, in Definitions]
R
rc_ctx [definition, in Framework]realizor [constructor, in RealizorPredicates]
realizorCandidate [definition, in RealizorPredicates]
realizorPredicate [record, in RealizorPredicates]
RealizorPredicates [library]
Reduction [library]
ren [definition, in Autosubst_Classes]
rename [projection, in Autosubst_Classes]
Rename [record, in Autosubst_Classes]
rename [constructor, in Autosubst_Classes]
Rename [inductive, in Autosubst_Classes]
Rename_Tterm [instance, in T1]
rename_subst [projection, in Autosubst_Classes]
rename_substX [lemma, in Autosubst_Tactics]
Rename_ftype [instance, in F1]
Rename_term [instance, in Definitions]
renS [lemma, in Autosubst_Lemmas]
ren_uncomp [lemma, in Autosubst_Lemmas]
rpe [instance, in RealizorPredicates]
rp_preservation [definition, in Framework]
rp_nat [lemma, in T1]
rp_equiv [definition, in RealizorPredicates]
S
S [constructor, in CL1]scomp [definition, in Autosubst_Classes]
scomp_hcompR [lemma, in Autosubst_Tactics]
scomp_hcompX [lemma, in Autosubst_Tactics]
scomp_hcompI [lemma, in Autosubst_Tactics]
scons [definition, in Autosubst_Basics]
scons_eta [lemma, in Autosubst_Basics]
scons_comp [lemma, in Autosubst_Basics]
simpletype [inductive, in STLC1]
simpletype [inductive, in CL1]
sn [lemma, in Framework]
SN [definition, in Reduction]
sn_tsn [lemma, in Framework]
sn_stlc [lemma, in STLC1]
sn_T [lemma, in T1]
sn_gsn [lemma, in Reduction]
sn_system [lemma, in Termination]
sn_F [lemma, in F1]
step [inductive, in Reduction]
steps [inductive, in Reduction]
steps_appR [lemma, in Reduction]
steps_appL [lemma, in Reduction]
step_beta_eq [lemma, in Reduction]
step_lam [constructor, in Reduction]
step_appR [constructor, in Reduction]
step_appL [constructor, in Reduction]
step_beta [constructor, in Reduction]
step_ty [lemma, in Termination]
step_n [lemma, in Termination]
stlctyapp [constructor, in STLC1]
stlctylam [constructor, in STLC1]
stlctyvar [constructor, in STLC1]
stlc_ty [inductive, in STLC1]
stlc_ctx [definition, in STLC1]
STLC1 [library]
subst [projection, in Autosubst_Classes]
Subst [record, in Autosubst_Classes]
subst [constructor, in Autosubst_Classes]
Subst [inductive, in Autosubst_Classes]
SubstHSubstComp [record, in Autosubst_Classes]
SubstHSubstComp [inductive, in Autosubst_Classes]
Substitution [library]
SubstLemmas [record, in Autosubst_Classes]
SubstLemmas [section, in Autosubst_Lemmas]
SubstLemmas_Tterm [instance, in T1]
SubstLemmas_ftype [instance, in F1]
SubstLemmas_term [instance, in Definitions]
Subst_Tterm [instance, in T1]
subst_hsubst_comp [projection, in Autosubst_Classes]
subst_hsubst_comp [constructor, in Autosubst_Classes]
subst_comp [projection, in Autosubst_Classes]
subst_id [projection, in Autosubst_Classes]
subst_compR [lemma, in Autosubst_Tactics]
subst_compX [lemma, in Autosubst_Tactics]
subst_compI [lemma, in Autosubst_Tactics]
subst_idX [lemma, in Autosubst_Tactics]
Subst_ftype [instance, in F1]
Subst_term [instance, in Definitions]
subsumes [definition, in Definitions]
Subsumption [library]
sub_inv_int [lemma, in Subsumption]
sub_inv_F_G [lemma, in Subsumption]
sub_inv [lemma, in Subsumption]
sub_inv_O [lemma, in Subsumption]
sub_inv_A [lemma, in Subsumption]
sub_proper [instance, in Subsumption]
sub_comp_int [lemma, in Subsumption]
sub_Int_R [lemma, in Subsumption]
sub_Int_L [lemma, in Subsumption]
sub_O [lemma, in Subsumption]
sub_int [lemma, in Subsumption]
sub_equiv [lemma, in Subsumption]
sub_preorder [instance, in Subsumption]
sub_trans [lemma, in Subsumption]
sub_refl [lemma, in Subsumption]
S_nat [constructor, in T1]
T
Tapp [constructor, in T1]TappL [constructor, in T1]
TappR [constructor, in T1]
Tbeta [constructor, in T1]
tcount [definition, in TypeEquivalence]
TC_c [lemma, in T1]
term [inductive, in Definitions]
Termination [library]
te_inv_incl [lemma, in Subsumption]
te_sub [instance, in Subsumption]
te_assoc_Int_rl [constructor, in Definitions]
te_assoc_Int_lr [constructor, in Definitions]
te_trans_ABC [constructor, in Definitions]
te_cong_Int [constructor, in Definitions]
te_comm_Int [constructor, in Definitions]
te_refl_OMEGA [constructor, in Definitions]
te_refl_F [constructor, in Definitions]
te_inv [lemma, in TypeEquivalence]
te_tcount_stable [lemma, in TypeEquivalence]
te_assoc_int [lemma, in TypeEquivalence]
te_comm_int [lemma, in TypeEquivalence]
te_Proper_int [instance, in TypeEquivalence]
te_comp_int [lemma, in TypeEquivalence]
te_comp_int_r [lemma, in TypeEquivalence]
te_comp_int_l [lemma, in TypeEquivalence]
te_inv_F [lemma, in TypeEquivalence]
te_O_r [lemma, in TypeEquivalence]
te_O_l [lemma, in TypeEquivalence]
te_inv_A [lemma, in TypeEquivalence]
te_inv_OMEGA [lemma, in TypeEquivalence]
te_equiv [instance, in TypeEquivalence]
te_trans [lemma, in TypeEquivalence]
te_sym [lemma, in TypeEquivalence]
te_refl [lemma, in TypeEquivalence]
Tlam [constructor, in T1]
TO [constructor, in T1]
top [definition, in Filters]
top_sigma_valuation [lemma, in Framework]
top_sigma [definition, in Framework]
top_rho_valid [lemma, in Framework]
top_rho [definition, in Framework]
top_nat [constructor, in T1]
top_app [lemma, in Filters]
top_filter [lemma, in Filters]
top_rp_realizable [lemma, in RealizorPredicates]
top_rp [definition, in RealizorPredicates]
Tprec [constructor, in T1]
TprecO [constructor, in T1]
TprecS [constructor, in T1]
translates [definition, in F1]
translates_skip [lemma, in F1]
TS [constructor, in T1]
tsn [lemma, in Framework]
TSN [definition, in Framework]
Tterm [inductive, in T1]
Ttyapp [constructor, in T1]
Ttylam [constructor, in T1]
TtyO [constructor, in T1]
Ttype [inductive, in T1]
Ttyprec [constructor, in T1]
TtyS [constructor, in T1]
Ttyvar [constructor, in T1]
Tvar [constructor, in T1]
tvar [constructor, in F1]
TVar [constructor, in Definitions]
ty [inductive, in Definitions]
tyAbs [constructor, in Definitions]
tyApp [constructor, in Definitions]
tycsub [lemma, in Types]
tyInt [constructor, in Definitions]
tymon [lemma, in Types]
tyO [constructor, in Definitions]
type [inductive, in Definitions]
typeable [definition, in T1]
TypeEquivalence [library]
Types [library]
type_equiv [inductive, in Definitions]
type_context [definition, in Interpretation]
tyren [inductive, in Weakening]
tyrenInv [constructor, in Weakening]
tyren_split [lemma, in Weakening]
tyren_var [lemma, in Weakening]
tyren_up [lemma, in Weakening]
tysub [inductive, in Substitution]
tysubA [lemma, in Types]
tysubCons [constructor, in Substitution]
tysubRen [constructor, in Substitution]
tysubst [lemma, in Substitution]
tysubst_var [lemma, in Substitution]
tysub_split [lemma, in Substitution]
tysub_up [lemma, in Substitution]
tysub_lift [lemma, in Substitution]
tysub_beta [lemma, in Substitution]
tyVar [constructor, in Definitions]
tyVarA [lemma, in Types]
tyVarU [lemma, in Types]
ty_S [lemma, in T1]
ty_equiv [lemma, in Types]
ty_subsume [lemma, in Types]
t_ctx [definition, in Framework]
T_valid [lemma, in T1]
T_ty [inductive, in T1]
T_ctx [definition, in T1]
T_step [inductive, in T1]
T1 [library]
U
up [definition, in Autosubst_Classes]UpB [constructor, in Definitions]
upE [lemma, in Autosubst_Tactics]
UpI [constructor, in Definitions]
upn [abbreviation, in Autosubst_Classes]
upren [definition, in Autosubst_Classes]
upX [lemma, in Autosubst_Tactics]
up_comp_n [lemma, in Autosubst_Lemmas]
up_comp [lemma, in Autosubst_Lemmas]
up_liftn [lemma, in Autosubst_Lemmas]
up_lift1 [lemma, in Autosubst_Lemmas]
up_id_n [lemma, in Autosubst_Lemmas]
up_id [lemma, in Autosubst_Lemmas]
up_hcomp_n_internal [lemma, in Autosubst_Derive]
up_hcomp_internal [lemma, in Autosubst_Derive]
up_comp_n_internal [lemma, in Autosubst_Derive]
up_comp_internal [lemma, in Autosubst_Derive]
up_comp_subst_ren_n_internal [lemma, in Autosubst_Derive]
up_comp_subst_ren_internal [lemma, in Autosubst_Derive]
up_comp_ren_subst_n [lemma, in Autosubst_Derive]
up_comp_ren_subst [lemma, in Autosubst_Derive]
up_id_n_internal [lemma, in Autosubst_Derive]
up_id_internal [lemma, in Autosubst_Derive]
up_upren_n_internal [lemma, in Autosubst_Derive]
up_upren_internal [lemma, in Autosubst_Derive]
V
valid [definition, in Interpretation]validates [definition, in Framework]
validates_up [lemma, in Framework]
validates_skip [lemma, in F1]
validation [definition, in Framework]
valid_up [lemma, in Interpretation]
valuation [definition, in Framework]
valuation_up [lemma, in Framework]
val_ty_v [lemma, in Framework]
val_ty_gamma [constructor, in Framework]
val_ty [inductive, in Framework]
val_ty_gamma [constructor, in T1]
val_ty [inductive, in T1]
var [definition, in Autosubst_Basics]
W
weaken [lemma, in Weakening]weakening [lemma, in Weakening]
Weakening [library]
X
xe_closure [lemma, in Filters]_
_bind [definition, in Autosubst_Classes]other
{ bind _ } (bind_scope) [notation, in Autosubst_Classes]{ bind _ in _ } (bind_scope) [notation, in Autosubst_Classes]
{ bind _ of _ } (bind_scope) [notation, in Autosubst_Classes]
{ bind _ of _ in _ } (bind_scope) [notation, in Autosubst_Classes]
_ ..|[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..|[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..|[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ .|[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .|[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .|[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ >>| _ (subst_scope) [notation, in Autosubst_Classes]
_ ..[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ .[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ >> _ (subst_scope) [notation, in Autosubst_Classes]
_ .: _ (subst_scope) [notation, in Autosubst_Basics]
_ >>> _ (subst_scope) [notation, in Autosubst_Basics]
_ == _ (type_scope) [notation, in Definitions]
_ ==> _ [notation, in T1]
_ --> _ [notation, in T1]
_ ~ _ [notation, in Filters]
_ @ _ [notation, in Filters]
_ >=1 _ [notation, in Definitions]
_ ==1 _ [notation, in Definitions]
_ =1 _ [notation, in Definitions]
_ & _ [notation, in Definitions]
_ >= _ [notation, in Definitions]
_ * _ [notation, in Definitions]
_ o _ [notation, in Definitions]
_ --> _ [notation, in Definitions]
_ --> _ [notation, in CL1]
_ =R= _ [notation, in RealizorPredicates]
' _ [notation, in T1]
( + _ ) [notation, in Autosubst_Basics]
[ _ ] _ [notation, in Interpretation]
[[ _ ]] _ [notation, in STLC1]
[[ _ ]] [notation, in T1]
[[ _ ]] _ [notation, in F1]
[[ _ ]] _ [notation, in CL1]
Instance Index
C
cequi_typep [in Types]csub_cint_proper [in Contexts]
cte_csub [in Contexts]
cte_cint_proper [in Contexts]
cte_equivalence [in Contexts]
D
decide_lt_nat [in Decidable]decide_le_nat [in Decidable]
decide_eq_nat [in Decidable]
E
equiv_comp_p [in Filters]equiv_e [in Filters]
equiv_rp_p [in RealizorPredicates]
equi_typep [in Types]
F
FV_dec [in Freevars]I
Ids_Tterm [in T1]Ids_ftype [in F1]
Ids_term [in Definitions]
int_equiv [in RealizorPredicates]
M
MMapExt_const [in Autosubst_MMap]MMapExt_refl [in Autosubst_MMap]
MMapExt_fun [in Autosubst_MMapInstances]
MMapExt_pair [in Autosubst_MMapInstances]
MMapExt_list [in Autosubst_MMapInstances]
MMapExt_option [in Autosubst_MMapInstances]
MMapLemmas_const [in Autosubst_MMap]
MMapLemmas_refl [in Autosubst_MMap]
MMapLemmas_fun [in Autosubst_MMapInstances]
MMapLemmas_pair [in Autosubst_MMapInstances]
MMapLemmas_list [in Autosubst_MMapInstances]
MMapLemmas_option [in Autosubst_MMapInstances]
MMap_const [in Autosubst_MMap]
MMap_refl [in Autosubst_MMap]
MMap_fun [in Autosubst_MMapInstances]
MMap_pair [in Autosubst_MMapInstances]
MMap_list [in Autosubst_MMapInstances]
MMap_option [in Autosubst_MMapInstances]
P
prod_equiv [in RealizorPredicates]R
Rename_Tterm [in T1]Rename_ftype [in F1]
Rename_term [in Definitions]
rpe [in RealizorPredicates]
S
SubstLemmas_Tterm [in T1]SubstLemmas_ftype [in F1]
SubstLemmas_term [in Definitions]
Subst_Tterm [in T1]
Subst_ftype [in F1]
Subst_term [in Definitions]
sub_proper [in Subsumption]
sub_preorder [in Subsumption]
T
te_sub [in Subsumption]te_Proper_int [in TypeEquivalence]
te_equiv [in TypeEquivalence]
Projection Index
C
closed_leu [in Filters]closed_int [in Filters]
D
decide [in Decidable]E
equiv_closed [in RealizorPredicates]excl_bot [in RealizorPredicates]
H
hsubst [in Autosubst_Classes]hsubst_hsubst_ind [in Autosubst_Classes]
hsubst_hsubst_comp [in Autosubst_Classes]
hsubst_comp [in Autosubst_Classes]
hsubst_id [in Autosubst_Classes]
I
ids [in Autosubst_Classes]id_hsubst [in Autosubst_Classes]
id_subst [in Autosubst_Classes]
incl_top [in RealizorPredicates]
M
mmap [in Autosubst_MMap]mmap_comp [in Autosubst_MMap]
mmap_id [in Autosubst_MMap]
mmap_ext [in Autosubst_MMap]
O
only_filter [in RealizorPredicates]R
rename [in Autosubst_Classes]rename_subst [in Autosubst_Classes]
S
subst [in Autosubst_Classes]subst_hsubst_comp [in Autosubst_Classes]
subst_comp [in Autosubst_Classes]
subst_id [in Autosubst_Classes]
Record Index
D
Dec [in Decidable]H
HSubst [in Autosubst_Classes]HSubstHSubstComp [in Autosubst_Classes]
HSubstHSubstInd [in Autosubst_Classes]
HSubstLemmas [in Autosubst_Classes]
I
Ids [in Autosubst_Classes]IFilter [in Filters]
M
MMap [in Autosubst_MMap]MMapExt [in Autosubst_MMap]
MMapLemmas [in Autosubst_MMap]
R
realizorPredicate [in RealizorPredicates]Rename [in Autosubst_Classes]
S
Subst [in Autosubst_Classes]SubstHSubstComp [in Autosubst_Classes]
SubstLemmas [in Autosubst_Classes]
Lemma Index
A
adequacy_cadequacy [in Framework]agree_equiv [in Freevars]
agree_ty [in Freevars]
B
bot_filter [in Filters]C
cint_csub_r [in Contexts]cint_csub_l [in Contexts]
cint_Empty [in Contexts]
cint_Gamma_Empty [in Contexts]
cint_Empty_Gamma [in Contexts]
CLC_c [in CL1]
closure_closure_equiv [in Filters]
closure_filter_equiv [in Filters]
closure_filter [in Filters]
CL_stlc [in CL1]
CL_valid [in CL1]
compA [in Autosubst_Basics]
compatible_sub [in Interpretation]
compatible_sub_Gamma [in Interpretation]
compatible_cint [in Interpretation]
compatible_down [in Interpretation]
compatible_up [in Interpretation]
compile_subst [in T1]
compile_subst_full [in T1]
compile_ren_full [in T1]
comp_id [in Autosubst_Basics]
conj' [in Autosubst_Basics]
cons_drop_inv [in Contexts]
csplit [in Contexts]
csub_ext [in Contexts]
csub_cint_comp [in Contexts]
csub_comm [in Contexts]
csub_sub [in Contexts]
cte_eq [in Contexts]
cte_ext_int [in Contexts]
cte_ext [in Contexts]
cte_csub_R [in Contexts]
cte_csub_L [in Contexts]
cte_csub_equiv [in Contexts]
cte_trans [in Contexts]
cte_sym [in Contexts]
cte_pwr_refl [in Contexts]
cte_refl [in Contexts]
cte_comp_cint [in Contexts]
cte_assoc_cint [in Contexts]
cte_comm_cint [in Contexts]
E
equal_f [in Autosubst_Basics]equiv_app_comp [in Filters]
equiv_filter [in Filters]
equiv_closure [in Filters]
equi_type [in Types]
F
feq_eq [in Contexts]feq_trans [in Contexts]
feq_ext_int [in Contexts]
feq_ext [in Contexts]
filter_filter_equiv [in Filters]
filter_equiv_trans [in Filters]
filter_equiv_sym [in Filters]
filter_equiv_refl [in Filters]
filter_ind_filter [in Filters]
fold_ren_cons [in Autosubst_Tactics]
fromclosure_F [in Filters]
H
hcomp_dist_internal [in Autosubst_Derive]hcomp_ren_internal [in Autosubst_Derive]
hcomp_lift_internal [in Autosubst_Derive]
hcomp_lift_n_internal [in Autosubst_Derive]
hsubst_compR [in Autosubst_Tactics]
hsubst_compX [in Autosubst_Tactics]
hsubst_compI [in Autosubst_Tactics]
hsubst_idX [in Autosubst_Tactics]
I
id_hsubstR [in Autosubst_Tactics]id_hsubstX [in Autosubst_Tactics]
id_scompR [in Autosubst_Tactics]
id_scompX [in Autosubst_Tactics]
id_comp [in Autosubst_Basics]
inclosure_F [in Filters]
incl_inv_sub [in Subsumption]
intersect_realizable [in RealizorPredicates]
int_lam [in Premodel]
int_st [in Premodel]
int_x [in Premodel]
int_ty_rp [in STLC1]
int_ty_rp [in T1]
int_nat_filter [in T1]
int_ty_beta [in F1]
int_ty_subst_equiv [in F1]
int_ty_ren_equiv [in F1]
int_ty_feq_equiv [in F1]
int_ty_rp [in F1]
int_ty_rp [in CL1]
int_eq_O [in TypeEquivalence]
int_comm_O [in TypeEquivalence]
int_O [in TypeEquivalence]
int_IF [in Interpretation]
invtyInt [in Types]
invtyVar [in Types]
in_int_ty [in STLC1]
in_int_ty [in T1]
in_int_ty [in F1]
in_int_ty [in CL1]
iterate_0 [in Autosubst_Basics]
iterate_S [in Autosubst_Basics]
iter_param [in Autosubst_Derive]
iter_fp [in Autosubst_Derive]
K
k_nat [in T1]L
lcc_c [in Framework]lift_injn [in Autosubst_Lemmas]
lift_inj [in Autosubst_Lemmas]
lift_eta [in Autosubst_Basics]
lift_compR [in Autosubst_Basics]
lift_comp [in Autosubst_Basics]
lift_scons [in Autosubst_Basics]
lift0 [in Autosubst_Lemmas]
lift0 [in Autosubst_Basics]
M
mmap_const_instE [in Autosubst_MMap]mmap_id_instE [in Autosubst_MMap]
mmap_compR [in Autosubst_MMap]
mmap_compX [in Autosubst_MMap]
mmap_idX [in Autosubst_MMap]
mmap_id_ext [in Autosubst_Derive]
P
plusA [in Autosubst_Basics]plusnO [in Autosubst_Basics]
plusnS [in Autosubst_Basics]
plusOn [in Autosubst_Basics]
plusSn [in Autosubst_Basics]
possible_int_specialize [in RealizorPredicates]
possible_int_realizable [in RealizorPredicates]
prod_realizable [in RealizorPredicates]
R
rename_substX [in Autosubst_Tactics]renS [in Autosubst_Lemmas]
ren_uncomp [in Autosubst_Lemmas]
rp_nat [in T1]
S
scomp_hcompR [in Autosubst_Tactics]scomp_hcompX [in Autosubst_Tactics]
scomp_hcompI [in Autosubst_Tactics]
scons_eta [in Autosubst_Basics]
scons_comp [in Autosubst_Basics]
sn [in Framework]
sn_tsn [in Framework]
sn_stlc [in STLC1]
sn_T [in T1]
sn_gsn [in Reduction]
sn_system [in Termination]
sn_F [in F1]
steps_appR [in Reduction]
steps_appL [in Reduction]
step_beta_eq [in Reduction]
step_ty [in Termination]
step_n [in Termination]
subst_compR [in Autosubst_Tactics]
subst_compX [in Autosubst_Tactics]
subst_compI [in Autosubst_Tactics]
subst_idX [in Autosubst_Tactics]
sub_inv_int [in Subsumption]
sub_inv_F_G [in Subsumption]
sub_inv [in Subsumption]
sub_inv_O [in Subsumption]
sub_inv_A [in Subsumption]
sub_comp_int [in Subsumption]
sub_Int_R [in Subsumption]
sub_Int_L [in Subsumption]
sub_O [in Subsumption]
sub_int [in Subsumption]
sub_equiv [in Subsumption]
sub_trans [in Subsumption]
sub_refl [in Subsumption]
T
TC_c [in T1]te_inv_incl [in Subsumption]
te_inv [in TypeEquivalence]
te_tcount_stable [in TypeEquivalence]
te_assoc_int [in TypeEquivalence]
te_comm_int [in TypeEquivalence]
te_comp_int [in TypeEquivalence]
te_comp_int_r [in TypeEquivalence]
te_comp_int_l [in TypeEquivalence]
te_inv_F [in TypeEquivalence]
te_O_r [in TypeEquivalence]
te_O_l [in TypeEquivalence]
te_inv_A [in TypeEquivalence]
te_inv_OMEGA [in TypeEquivalence]
te_trans [in TypeEquivalence]
te_sym [in TypeEquivalence]
te_refl [in TypeEquivalence]
top_sigma_valuation [in Framework]
top_rho_valid [in Framework]
top_app [in Filters]
top_filter [in Filters]
top_rp_realizable [in RealizorPredicates]
translates_skip [in F1]
tsn [in Framework]
tycsub [in Types]
tymon [in Types]
tyren_split [in Weakening]
tyren_var [in Weakening]
tyren_up [in Weakening]
tysubA [in Types]
tysubst [in Substitution]
tysubst_var [in Substitution]
tysub_split [in Substitution]
tysub_up [in Substitution]
tysub_lift [in Substitution]
tysub_beta [in Substitution]
tyVarA [in Types]
tyVarU [in Types]
ty_S [in T1]
ty_equiv [in Types]
ty_subsume [in Types]
T_valid [in T1]
U
upE [in Autosubst_Tactics]upX [in Autosubst_Tactics]
up_comp_n [in Autosubst_Lemmas]
up_comp [in Autosubst_Lemmas]
up_liftn [in Autosubst_Lemmas]
up_lift1 [in Autosubst_Lemmas]
up_id_n [in Autosubst_Lemmas]
up_id [in Autosubst_Lemmas]
up_hcomp_n_internal [in Autosubst_Derive]
up_hcomp_internal [in Autosubst_Derive]
up_comp_n_internal [in Autosubst_Derive]
up_comp_internal [in Autosubst_Derive]
up_comp_subst_ren_n_internal [in Autosubst_Derive]
up_comp_subst_ren_internal [in Autosubst_Derive]
up_comp_ren_subst_n [in Autosubst_Derive]
up_comp_ren_subst [in Autosubst_Derive]
up_id_n_internal [in Autosubst_Derive]
up_id_internal [in Autosubst_Derive]
up_upren_n_internal [in Autosubst_Derive]
up_upren_internal [in Autosubst_Derive]
V
validates_up [in Framework]validates_skip [in F1]
valid_up [in Interpretation]
valuation_up [in Framework]
val_ty_v [in Framework]
W
weaken [in Weakening]weakening [in Weakening]
X
xe_closure [in Filters]Section Index
G
General_Termination.LambdaCurry [in Framework]General_Termination.Compiler [in Framework]
General_Termination [in Framework]
I
InternalLemmas [in Autosubst_Derive]InternalLemmasHSubst [in Autosubst_Derive]
L
LemmasForFun [in Autosubst_Basics]LemmasForHSubst [in Autosubst_Tactics]
LemmasForMMap [in Autosubst_MMap]
LemmasForSubst [in Autosubst_Tactics]
M
MMapConst [in Autosubst_MMap]MMapId [in Autosubst_MMap]
MMapInstances [in Autosubst_MMapInstances]
S
SubstLemmas [in Autosubst_Lemmas]Constructor Index
A
App [in Definitions]app [in CL1]
arr [in STLC1]
arr [in T1]
arr [in F1]
Arr [in Definitions]
arr [in CL1]
B
base [in STLC1]BASE [in Definitions]
base [in CL1]
C
CLapp [in CL1]CLK [in CL1]
CLS [in CL1]
cl_step_appR [in CL1]
cl_step_appL [in CL1]
cl_stepK [in CL1]
cl_stepS [in CL1]
D
decide [in Decidable]F
fapp [in F1]fgen [in F1]
flam [in F1]
fspec [in F1]
FVAppL [in Freevars]
FVAppR [in Freevars]
fvar [in F1]
FVLam [in Freevars]
FVVar [in Freevars]
G
gsn [in Reduction]H
hsubst [in Autosubst_Classes]hsubst_hsubst_ind [in Autosubst_Classes]
hsubst_hsubst_comp [in Autosubst_Classes]
I
ids [in Autosubst_Classes]inApp [in Filters]
includesDropL [in Subsumption]
includesDropR [in Subsumption]
includesF [in Subsumption]
inF [in Filters]
inI [in Filters]
inKtype [in T1]
Int [in Definitions]
intty [in Interpretation]
K
K [in CL1]L
Lam [in Definitions]M
mmap [in Autosubst_MMap]mmap_ext [in Autosubst_MMap]
more [in Reduction]
N
NAT [in T1]O
OMEGA [in Definitions]one [in Reduction]
O_nat [in T1]
P
pi [in F1]R
realizor [in RealizorPredicates]rename [in Autosubst_Classes]
S
S [in CL1]step_lam [in Reduction]
step_appR [in Reduction]
step_appL [in Reduction]
step_beta [in Reduction]
stlctyapp [in STLC1]
stlctylam [in STLC1]
stlctyvar [in STLC1]
subst [in Autosubst_Classes]
subst_hsubst_comp [in Autosubst_Classes]
S_nat [in T1]
T
Tapp [in T1]TappL [in T1]
TappR [in T1]
Tbeta [in T1]
te_assoc_Int_rl [in Definitions]
te_assoc_Int_lr [in Definitions]
te_trans_ABC [in Definitions]
te_cong_Int [in Definitions]
te_comm_Int [in Definitions]
te_refl_OMEGA [in Definitions]
te_refl_F [in Definitions]
Tlam [in T1]
TO [in T1]
top_nat [in T1]
Tprec [in T1]
TprecO [in T1]
TprecS [in T1]
TS [in T1]
Ttyapp [in T1]
Ttylam [in T1]
TtyO [in T1]
Ttyprec [in T1]
TtyS [in T1]
Ttyvar [in T1]
Tvar [in T1]
tvar [in F1]
TVar [in Definitions]
tyAbs [in Definitions]
tyApp [in Definitions]
tyInt [in Definitions]
tyO [in Definitions]
tyrenInv [in Weakening]
tysubCons [in Substitution]
tysubRen [in Substitution]
tyVar [in Definitions]
U
UpB [in Definitions]UpI [in Definitions]
V
val_ty_gamma [in Framework]val_ty_gamma [in T1]
Notation Index
G
[| _ |] [in Framework][[ _ ]] _ [in Framework]
other
{ bind _ } (bind_scope) [in Autosubst_Classes]{ bind _ in _ } (bind_scope) [in Autosubst_Classes]
{ bind _ of _ } (bind_scope) [in Autosubst_Classes]
{ bind _ of _ in _ } (bind_scope) [in Autosubst_Classes]
_ ..|[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ ..|[ _ /] (subst_scope) [in Autosubst_Classes]
_ ..|[ _ ] (subst_scope) [in Autosubst_Classes]
_ .|[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ .|[ _ /] (subst_scope) [in Autosubst_Classes]
_ .|[ _ ] (subst_scope) [in Autosubst_Classes]
_ >>| _ (subst_scope) [in Autosubst_Classes]
_ ..[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ ..[ _ /] (subst_scope) [in Autosubst_Classes]
_ ..[ _ ] (subst_scope) [in Autosubst_Classes]
_ .[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ .[ _ /] (subst_scope) [in Autosubst_Classes]
_ .[ _ ] (subst_scope) [in Autosubst_Classes]
_ >> _ (subst_scope) [in Autosubst_Classes]
_ .: _ (subst_scope) [in Autosubst_Basics]
_ >>> _ (subst_scope) [in Autosubst_Basics]
_ == _ (type_scope) [in Definitions]
_ ==> _ [in T1]
_ --> _ [in T1]
_ ~ _ [in Filters]
_ @ _ [in Filters]
_ >=1 _ [in Definitions]
_ ==1 _ [in Definitions]
_ =1 _ [in Definitions]
_ & _ [in Definitions]
_ >= _ [in Definitions]
_ * _ [in Definitions]
_ o _ [in Definitions]
_ --> _ [in Definitions]
_ --> _ [in CL1]
_ =R= _ [in RealizorPredicates]
' _ [in T1]
( + _ ) [in Autosubst_Basics]
[ _ ] _ [in Interpretation]
[[ _ ]] _ [in STLC1]
[[ _ ]] [in T1]
[[ _ ]] _ [in F1]
[[ _ ]] _ [in CL1]
Inductive Index
A
app [in Filters]B
basetype [in Definitions]C
CL [in CL1]closure [in Filters]
cl_step [in CL1]
CL_ty [in CL1]
D
Dec [in Decidable]F
Ftype [in F1]FV [in Freevars]
f_ty [in F1]
G
GSN [in Reduction]H
HSubst [in Autosubst_Classes]HSubstHSubstComp [in Autosubst_Classes]
HSubstHSubstInd [in Autosubst_Classes]
I
Ids [in Autosubst_Classes]includes [in Subsumption]
inttype [in Definitions]
int_nat [in T1]
int_t [in Interpretation]
K
Ktype [in T1]M
MMap [in Autosubst_MMap]MMapExt [in Autosubst_MMap]
R
Rename [in Autosubst_Classes]S
simpletype [in STLC1]simpletype [in CL1]
step [in Reduction]
steps [in Reduction]
stlc_ty [in STLC1]
Subst [in Autosubst_Classes]
SubstHSubstComp [in Autosubst_Classes]
T
term [in Definitions]Tterm [in T1]
Ttype [in T1]
ty [in Definitions]
type [in Definitions]
type_equiv [in Definitions]
tyren [in Weakening]
tysub [in Substitution]
T_ty [in T1]
T_step [in T1]
V
val_ty [in Framework]val_ty [in T1]
Abbreviation Index
U
upn [in Autosubst_Classes]Definition Index
A
adequacy [in Framework]annot [in Autosubst_Basics]
B
bot [in Filters]C
cadequacy [in Framework]cint [in Definitions]
CLC [in CL1]
compatible [in Interpretation]
compile [in T1]
compiler_consistency [in Framework]
context [in Definitions]
count [in TypeEquivalence]
csub [in Definitions]
cte [in Definitions]
D
dec [in Decidable]drop [in Definitions]
E
Empty [in Definitions]F
filter_equiv [in Filters]funcomp [in Autosubst_Basics]
f_ctx [in F1]
H
hcomp [in Autosubst_Classes]I
id [in Autosubst_Basics]inc [in Weakening]
int [in Definitions]
intersect [in RealizorPredicates]
int_ty [in STLC1]
int_ty [in T1]
int_ty [in F1]
int_app [in Filters]
int_ty [in CL1]
iterate [in Autosubst_Basics]
L
lcc [in Framework]lift [in Autosubst_Basics]
P
pi_equiv [in RealizorPredicates]possible_int [in RealizorPredicates]
prod [in RealizorPredicates]
PWR [in Definitions]
R
rc_ctx [in Framework]realizorCandidate [in RealizorPredicates]
ren [in Autosubst_Classes]
rp_preservation [in Framework]
rp_equiv [in RealizorPredicates]
S
scomp [in Autosubst_Classes]scons [in Autosubst_Basics]
SN [in Reduction]
stlc_ctx [in STLC1]
subsumes [in Definitions]
T
tcount [in TypeEquivalence]top [in Filters]
top_sigma [in Framework]
top_rho [in Framework]
top_rp [in RealizorPredicates]
translates [in F1]
TSN [in Framework]
typeable [in T1]
type_context [in Interpretation]
t_ctx [in Framework]
T_ctx [in T1]
U
up [in Autosubst_Classes]upren [in Autosubst_Classes]
V
valid [in Interpretation]validates [in Framework]
validation [in Framework]
valuation [in Framework]
var [in Autosubst_Basics]
_
_bind [in Autosubst_Classes]Variable Index
G
General_Termination.LambdaCurry.tty [in Framework]General_Termination.Compiler.tstep [in Framework]
General_Termination.Compiler.vtty [in Framework]
General_Termination.Compiler.ctty [in Framework]
General_Termination.Compiler.compiler [in Framework]
General_Termination.Compiler.tterm [in Framework]
General_Termination.int_ty [in Framework]
General_Termination.ttype [in Framework]
M
MMapInstances.A [in Autosubst_MMapInstances]MMapInstances.B [in Autosubst_MMapInstances]
MMapInstances.C [in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_C [in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_B [in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_C [in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_B [in Autosubst_MMapInstances]
MMapInstances.MMap_A_C [in Autosubst_MMapInstances]
MMapInstances.MMap_A_B [in Autosubst_MMapInstances]
Library Index
A
AutosubstAutosubst_MMapInstances
Autosubst_Classes
Autosubst_Derive
Autosubst_MMap
Autosubst_Tactics
Autosubst_Basics
Autosubst_Lemmas
C
CL1Contexts
D
DecidableDefinitions
F
FiltersFramework
Freevars
F1
F2
I
InterpretationP
PremodelR
RealizorPredicatesReduction
S
STLC1Substitution
Subsumption
T
TerminationTypeEquivalence
Types
T1
W
Weakening| 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 | (640 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 | (51 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 | (25 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 | (15 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 | (235 entries) |
| Section 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 | (13 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 | (103 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 | (44 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 | (42 entries) |
| Abbreviation 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) |
| 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 | (65 entries) |
| Variable 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) |
| 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 | (29 entries) |
This page has been generated by coqdoc