| 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 | (851 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 | (59 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 | (7 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 | (18 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 | (285 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 | (145 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) |
| 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 | (24 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 | (7 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 | (25 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 | (15 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 | (190 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 | (17 entries) |
Global Index
A
All [inductive, in LocalComp.Util]All_map [lemma, in LocalComp.Util]
All_prod [lemma, in LocalComp.Util]
All_forallb [lemma, in LocalComp.Util]
All_impl [lemma, in LocalComp.Util]
All_Forall [lemma, in LocalComp.Util]
All_sind [definition, in LocalComp.Util]
All_rec [definition, in LocalComp.Util]
All_ind [definition, in LocalComp.Util]
All_rect [definition, in LocalComp.Util]
All_cons [constructor, in LocalComp.Util]
All_nil [constructor, in LocalComp.Util]
ap [definition, in LocalComp.autosubst.unscoped]
apc [definition, in LocalComp.autosubst.unscoped]
apply_subst_sound [lemma, in LocalComp.autosubst.AST_rasimpl]
apply_subst [definition, in LocalComp.autosubst.AST_rasimpl]
apply_ren_sound [lemma, in LocalComp.autosubst.RAsimpl]
apply_ren [definition, in LocalComp.autosubst.RAsimpl]
apps [definition, in LocalComp.Inst]
aref [definition, in LocalComp.BasicAST]
Assm [constructor, in LocalComp.Env]
AST [library]
AST_preamble [library]
AST_rasimpl [library]
autosubst_simpl_styping [lemma, in LocalComp.BasicMetaTheory]
autosubst_simpl_rtyping [lemma, in LocalComp.BasicMetaTheory]
autosubst_simpl_term_subst [lemma, in LocalComp.autosubst.AST_rasimpl]
autosubst_simpl_term_ren [lemma, in LocalComp.autosubst.AST_rasimpl]
autosubst_simpl_csubst [projection, in LocalComp.autosubst.AST_rasimpl]
autosubst_simpl_term [projection, in LocalComp.autosubst.AST_rasimpl]
autosubst_simpl_ren [projection, in LocalComp.autosubst.RAsimpl]
B
BasicAST [library]BasicMetaTheory [library]
C
closed [abbreviation, in LocalComp.Typing]closed_instance [abbreviation, in LocalComp.Typing]
closed_inst [lemma, in LocalComp.BasicMetaTheory]
closed_lift_instance [lemma, in LocalComp.BasicMetaTheory]
closed_subst_instance [lemma, in LocalComp.BasicMetaTheory]
closed_subst [lemma, in LocalComp.BasicMetaTheory]
closed_ren_instance [lemma, in LocalComp.BasicMetaTheory]
closed_ren [lemma, in LocalComp.BasicMetaTheory]
clos_refl_sym_trans_incl [lemma, in LocalComp.Util]
CombineNotations [module, in LocalComp.autosubst.unscoped]
_ >> _ (fscope) [notation, in LocalComp.autosubst.unscoped]
_ .: _ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
Comp [constructor, in LocalComp.Env]
cong_const [constructor, in LocalComp.Typing]
cong_app [constructor, in LocalComp.Typing]
cong_lam [constructor, in LocalComp.Typing]
cong_Pi [constructor, in LocalComp.Typing]
cong_inst [lemma, in LocalComp.BasicMetaTheory]
conservativity [lemma, in LocalComp.Inlining]
conversion [inductive, in LocalComp.Typing]
conversion_sind [definition, in LocalComp.Typing]
conversion_ind [definition, in LocalComp.Typing]
conversion_ind [lemma, in LocalComp.BasicMetaTheory]
conv_trans [constructor, in LocalComp.Typing]
conv_sym [constructor, in LocalComp.Typing]
conv_refl [constructor, in LocalComp.Typing]
conv_red [constructor, in LocalComp.Typing]
conv_unfold [constructor, in LocalComp.Typing]
conv_beta [constructor, in LocalComp.Typing]
conv_gweak [lemma, in LocalComp.BasicMetaTheory]
conv_eweak [lemma, in LocalComp.BasicMetaTheory]
conv_insts [lemma, in LocalComp.BasicMetaTheory]
conv_inst_closed [lemma, in LocalComp.BasicMetaTheory]
conv_inst [lemma, in LocalComp.BasicMetaTheory]
conv_subst [lemma, in LocalComp.BasicMetaTheory]
conv_ren [lemma, in LocalComp.BasicMetaTheory]
conv_ctx_irr [lemma, in LocalComp.BasicMetaTheory]
conv_equiv [lemma, in LocalComp.Reduction]
conv_inline [lemma, in LocalComp.Inlining]
conv_ren_inst [lemma, in LocalComp.Inlining]
Core [module, in LocalComp.autosubst.AST]
core [library]
Core.app [constructor, in LocalComp.autosubst.AST]
Core.assm [constructor, in LocalComp.autosubst.AST]
Core.compRenRen_term [definition, in LocalComp.autosubst.AST]
Core.compRenSubst_term [definition, in LocalComp.autosubst.AST]
Core.compSubstRen_term [definition, in LocalComp.autosubst.AST]
Core.compSubstSubst_term [definition, in LocalComp.autosubst.AST]
Core.congr_assm [lemma, in LocalComp.autosubst.AST]
Core.congr_const [lemma, in LocalComp.autosubst.AST]
Core.congr_app [lemma, in LocalComp.autosubst.AST]
Core.congr_lam [lemma, in LocalComp.autosubst.AST]
Core.congr_Pi [lemma, in LocalComp.autosubst.AST]
Core.congr_Sort [lemma, in LocalComp.autosubst.AST]
Core.const [constructor, in LocalComp.autosubst.AST]
Core.extRen_term [definition, in LocalComp.autosubst.AST]
Core.ext_term [definition, in LocalComp.autosubst.AST]
Core.idSubst_term [definition, in LocalComp.autosubst.AST]
Core.instId'_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.instId'_term [lemma, in LocalComp.autosubst.AST]
Core.lam [constructor, in LocalComp.autosubst.AST]
Core.Pi [constructor, in LocalComp.autosubst.AST]
Core.renRen_term [lemma, in LocalComp.autosubst.AST]
Core.renRen'_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.renSubst_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.renSubst_term [lemma, in LocalComp.autosubst.AST]
Core.ren_term_morphism2 [instance, in LocalComp.autosubst.AST]
Core.ren_term_morphism [instance, in LocalComp.autosubst.AST]
Core.Ren_term [instance, in LocalComp.autosubst.AST]
Core.ren_term [definition, in LocalComp.autosubst.AST]
Core.rinstId'_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.rinstId'_term [lemma, in LocalComp.autosubst.AST]
Core.rinstInst_up_term_term [lemma, in LocalComp.autosubst.AST]
Core.rinstInst'_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.rinstInst'_term [lemma, in LocalComp.autosubst.AST]
Core.rinst_inst_term [definition, in LocalComp.autosubst.AST]
Core.Sort [constructor, in LocalComp.autosubst.AST]
Core.substRen_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.substRen_term [lemma, in LocalComp.autosubst.AST]
Core.substSubst_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.substSubst_term [lemma, in LocalComp.autosubst.AST]
Core.subst_term_morphism2 [instance, in LocalComp.autosubst.AST]
Core.subst_term_morphism [instance, in LocalComp.autosubst.AST]
Core.Subst_term [instance, in LocalComp.autosubst.AST]
Core.subst_term [definition, in LocalComp.autosubst.AST]
Core.term [inductive, in LocalComp.autosubst.AST]
Core.term_sind [definition, in LocalComp.autosubst.AST]
Core.term_rec [definition, in LocalComp.autosubst.AST]
Core.term_ind [definition, in LocalComp.autosubst.AST]
Core.term_rect [definition, in LocalComp.autosubst.AST]
Core.upExtRen_term_term [lemma, in LocalComp.autosubst.AST]
Core.upExt_term_term [lemma, in LocalComp.autosubst.AST]
Core.upId_term_term [lemma, in LocalComp.autosubst.AST]
Core.upRen_term_term [lemma, in LocalComp.autosubst.AST]
Core.Up_term_term [instance, in LocalComp.autosubst.AST]
Core.up_term [projection, in LocalComp.autosubst.AST]
Core.Up_term [record, in LocalComp.autosubst.AST]
Core.up_term [constructor, in LocalComp.autosubst.AST]
Core.Up_term [inductive, in LocalComp.autosubst.AST]
Core.up_subst_subst_term_term [lemma, in LocalComp.autosubst.AST]
Core.up_subst_ren_term_term [lemma, in LocalComp.autosubst.AST]
Core.up_ren_subst_term_term [lemma, in LocalComp.autosubst.AST]
Core.up_ren_ren_term_term [lemma, in LocalComp.autosubst.AST]
Core.up_term_term [lemma, in LocalComp.autosubst.AST]
Core.var [constructor, in LocalComp.autosubst.AST]
Core.VarInstance_term [instance, in LocalComp.autosubst.AST]
Core.varLRen'_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.varLRen'_term [lemma, in LocalComp.autosubst.AST]
Core.varL'_term_pointwise [lemma, in LocalComp.autosubst.AST]
Core.varL'_term [lemma, in LocalComp.autosubst.AST]
_ __term (subst_scope) [notation, in LocalComp.autosubst.AST]
_ __term (subst_scope) [notation, in LocalComp.autosubst.AST]
var (subst_scope) [notation, in LocalComp.autosubst.AST]
_ ⟨ _ ⟩ (subst_scope) [notation, in LocalComp.autosubst.AST]
↑__term (subst_scope) [notation, in LocalComp.autosubst.AST]
↑__term (subst_scope) [notation, in LocalComp.autosubst.AST]
_ [ _ ] (subst_scope) [notation, in LocalComp.autosubst.AST]
crule [record, in LocalComp.Env]
crule_eq [definition, in LocalComp.Env]
cr_typ [projection, in LocalComp.Env]
cr_rep [projection, in LocalComp.Env]
cr_sub [projection, in LocalComp.Env]
cr_pat [projection, in LocalComp.Env]
cr_env [projection, in LocalComp.Env]
cr_rep_inline [lemma, in LocalComp.Inlining]
cr_pat_inline [lemma, in LocalComp.Inlining]
ctx [definition, in LocalComp.Env]
ctx_inst_comp [lemma, in LocalComp.BasicMetaTheory]
ctx_inst_app [lemma, in LocalComp.BasicMetaTheory]
ctx_inst [definition, in LocalComp.Inst]
D
Def [constructor, in LocalComp.Env]diamond [lemma, in LocalComp.Pattern]
dummy [definition, in LocalComp.Inst]
E
Env [library]equation [record, in LocalComp.Env]
equations_typing_gscope [lemma, in LocalComp.GScope]
equation_typing [definition, in LocalComp.Typing]
equation_typing_gscope [lemma, in LocalComp.GScope]
equation_typing_gweak [lemma, in LocalComp.BasicMetaTheory]
equation_typing_eweak [lemma, in LocalComp.BasicMetaTheory]
equiv [definition, in LocalComp.Reduction]
equiv_const [lemma, in LocalComp.Reduction]
equiv_app [lemma, in LocalComp.Reduction]
equiv_lam [lemma, in LocalComp.Reduction]
equiv_Pi [lemma, in LocalComp.Reduction]
equiv_join [lemma, in LocalComp.Reduction]
equiv_red_ind [lemma, in LocalComp.Reduction]
equiv_trans [instance, in LocalComp.Reduction]
equiv_sym [instance, in LocalComp.Reduction]
equiv_refl [instance, in LocalComp.Reduction]
eq_subst_trunc [lemma, in LocalComp.BasicMetaTheory]
eq_subst_on_up [lemma, in LocalComp.BasicMetaTheory]
eq_subst_on [definition, in LocalComp.BasicMetaTheory]
eq_typ [projection, in LocalComp.Env]
eq_rhs [projection, in LocalComp.Env]
eq_lhs [projection, in LocalComp.Env]
eq_env [projection, in LocalComp.Env]
eq_gscope_gcons [lemma, in LocalComp.Inlining]
eq_gscope [definition, in LocalComp.Inlining]
ers_other [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_ren_r [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_cons_r [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_rcomp_r [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_compr_r [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_comp_r [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_id_r [constructor, in LocalComp.autosubst.AST_rasimpl]
ers_id_l [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_other [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_cons_shift [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_ren_l [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_cons_r [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_comp_r [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_id_r [constructor, in LocalComp.autosubst.AST_rasimpl]
esr_id_l [constructor, in LocalComp.autosubst.AST_rasimpl]
es_other [constructor, in LocalComp.autosubst.AST_rasimpl]
es_ren_r [constructor, in LocalComp.autosubst.AST_rasimpl]
es_ren_l [constructor, in LocalComp.autosubst.AST_rasimpl]
es_cons_r [constructor, in LocalComp.autosubst.AST_rasimpl]
es_rcomp_r [constructor, in LocalComp.autosubst.AST_rasimpl]
es_compr_r [constructor, in LocalComp.autosubst.AST_rasimpl]
es_comp_r [constructor, in LocalComp.autosubst.AST_rasimpl]
es_id_r [constructor, in LocalComp.autosubst.AST_rasimpl]
es_id_l [constructor, in LocalComp.autosubst.AST_rasimpl]
eval_term_sound [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_sound [definition, in LocalComp.autosubst.AST_rasimpl]
eval_term [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_c [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_sind [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_rec [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_ind [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_rect [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view [inductive, in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_c [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_sind [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_rec [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_ind [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_rect [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view [inductive, in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_c [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_sind [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_rec [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_ind [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_rect [definition, in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view [inductive, in LocalComp.autosubst.AST_rasimpl]
eval_ren_sound [lemma, in LocalComp.autosubst.RAsimpl]
eval_ren [definition, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_c [definition, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_sind [definition, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_rec [definition, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_ind [definition, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_rect [definition, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_other [constructor, in LocalComp.autosubst.RAsimpl]
eval_ren_cons_r [constructor, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_r [constructor, in LocalComp.autosubst.RAsimpl]
eval_ren_cons_shift [constructor, in LocalComp.autosubst.RAsimpl]
eval_ren_id_r [constructor, in LocalComp.autosubst.RAsimpl]
eval_ren_id_l [constructor, in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view [inductive, in LocalComp.autosubst.RAsimpl]
extends [definition, in LocalComp.Env]
extends_gcons [lemma, in LocalComp.BasicMetaTheory]
extends_nil [lemma, in LocalComp.BasicMetaTheory]
Extra [module, in LocalComp.autosubst.AST]
ext_term_scoped [lemma, in LocalComp.BasicMetaTheory]
F
fold_left_ext [lemma, in LocalComp.Util]fold_left_ind [lemma, in LocalComp.Util]
fold_left_map [lemma, in LocalComp.Util]
forallb_All [lemma, in LocalComp.Util]
forall_All [lemma, in LocalComp.Util]
Forall2_rst_OnOne2 [lemma, in LocalComp.Util]
Forall2_nth_error_l [lemma, in LocalComp.Util]
Forall2_diag [lemma, in LocalComp.Util]
Forall2_map_r [lemma, in LocalComp.Util]
Forall2_map_l [lemma, in LocalComp.Util]
funcomp [definition, in LocalComp.autosubst.core]
funcomp_morphism2 [instance, in LocalComp.autosubst.core]
funcomp_morphism [instance, in LocalComp.autosubst.core]
funcomp_assoc [lemma, in LocalComp.autosubst.core]
G
gclosed [definition, in LocalComp.Inlining]gcons [definition, in LocalComp.Inlining]
gcons_neq [lemma, in LocalComp.Inlining]
gcons_eq [lemma, in LocalComp.Inlining]
gctx [definition, in LocalComp.Env]
gctx_get [definition, in LocalComp.Env]
gdecl [inductive, in LocalComp.Env]
gdecl_sind [definition, in LocalComp.Env]
gdecl_rec [definition, in LocalComp.Env]
gdecl_ind [definition, in LocalComp.Env]
gdecl_rect [definition, in LocalComp.Env]
ginst [abbreviation, in LocalComp.Inlining]
gnil [definition, in LocalComp.Inlining]
gref [definition, in LocalComp.BasicAST]
gscope [inductive, in LocalComp.Typing]
GScope [library]
gscope_crule [definition, in LocalComp.Typing]
gscope_instance [abbreviation, in LocalComp.Typing]
gscope_sind [definition, in LocalComp.Typing]
gscope_ind [definition, in LocalComp.Typing]
gscope_assm [constructor, in LocalComp.Typing]
gscope_const [constructor, in LocalComp.Typing]
gscope_app [constructor, in LocalComp.Typing]
gscope_lam [constructor, in LocalComp.Typing]
gscope_pi [constructor, in LocalComp.Typing]
gscope_sort [constructor, in LocalComp.Typing]
gscope_var [constructor, in LocalComp.Typing]
gscope_apps_inv [lemma, in LocalComp.GScope]
gscope_equation [definition, in LocalComp.GScope]
gscope_crule_gweak [lemma, in LocalComp.BasicMetaTheory]
gscope_gweak [lemma, in LocalComp.BasicMetaTheory]
gscope_ind [lemma, in LocalComp.BasicMetaTheory]
gwf [inductive, in LocalComp.Typing]
gwf_sind [definition, in LocalComp.Typing]
gwf_ind [definition, in LocalComp.Typing]
gwf_def [constructor, in LocalComp.Typing]
gwf_nil [constructor, in LocalComp.Typing]
gwf_type [lemma, in LocalComp.Inlining]
gwf_conv_unfold [lemma, in LocalComp.Inlining]
gwf_gclosed [lemma, in LocalComp.Inlining]
g_type [definition, in LocalComp.Inlining]
g_conv_unfold [definition, in LocalComp.Inlining]
I
ictx [definition, in LocalComp.Env]ictx_get_case [lemma, in LocalComp.BasicMetaTheory]
ictx_get_weak [lemma, in LocalComp.BasicMetaTheory]
ictx_get [definition, in LocalComp.Env]
ictx_get_comp_inline [lemma, in LocalComp.Inlining]
ictx_get_assm_inline [lemma, in LocalComp.Inlining]
ictx_get_map [lemma, in LocalComp.Inlining]
id [definition, in LocalComp.autosubst.unscoped]
idecl [inductive, in LocalComp.Env]
idecl_sind [definition, in LocalComp.Env]
idecl_rec [definition, in LocalComp.Env]
idecl_ind [definition, in LocalComp.Env]
idecl_rect [definition, in LocalComp.Env]
ids [projection, in LocalComp.autosubst.unscoped]
ids [constructor, in LocalComp.autosubst.unscoped]
idsRen [instance, in LocalComp.autosubst.unscoped]
iget [definition, in LocalComp.Inst]
iget_subst [lemma, in LocalComp.BasicMetaTheory]
iget_ren [lemma, in LocalComp.BasicMetaTheory]
Injectivity [section, in LocalComp.Reduction]
Injectivity.hnopi [variable, in LocalComp.Reduction]
Injectivity.Ξ [variable, in LocalComp.Reduction]
Injectivity.Σ [variable, in LocalComp.Reduction]
inline [definition, in LocalComp.Inlining]
Inline [section, in LocalComp.Inlining]
inline_nil_id [lemma, in LocalComp.Inlining]
inline_ctx_ext [lemma, in LocalComp.Inlining]
inline_ictx_ext [lemma, in LocalComp.Inlining]
inline_crules_ext [lemma, in LocalComp.Inlining]
inline_crule_ext [lemma, in LocalComp.Inlining]
inline_list_ext [lemma, in LocalComp.Inlining]
inline_instance_ext [lemma, in LocalComp.Inlining]
inline_ext [lemma, in LocalComp.Inlining]
inline_gctx_ufd [definition, in LocalComp.Inlining]
inline_ctx_inst [lemma, in LocalComp.Inlining]
inline_inst [lemma, in LocalComp.Inlining]
inline_ren_instance [lemma, in LocalComp.Inlining]
inline_iget [lemma, in LocalComp.Inlining]
inline_subst [lemma, in LocalComp.Inlining]
inline_ren [lemma, in LocalComp.Inlining]
inline_idecl [definition, in LocalComp.Inlining]
inline_crule [definition, in LocalComp.Inlining]
Inline.hclosed [variable, in LocalComp.Inlining]
Inline.h_type [variable, in LocalComp.Inlining]
Inline.h_conv_unfold [variable, in LocalComp.Inlining]
⟦ _ ⟧e [notation, in LocalComp.Inlining]
⟦ _ ⟧d [notation, in LocalComp.Inlining]
⟦ _ ⟧R [notation, in LocalComp.Inlining]
⟦ _ ⟧r [notation, in LocalComp.Inlining]
⟦ _ ⟧* [notation, in LocalComp.Inlining]
⟦ _ ⟧× [notation, in LocalComp.Inlining]
⟦ _ ⟧ [notation, in LocalComp.Inlining]
Inline.Σ [variable, in LocalComp.Inlining]
Inline.κ [variable, in LocalComp.Inlining]
inlining [lemma, in LocalComp.Inlining]
Inlining [library]
inst [definition, in LocalComp.Inst]
Inst [library]
instance [definition, in LocalComp.Env]
inst_typing [abbreviation, in LocalComp.Typing]
inst_iget [abbreviation, in LocalComp.Typing]
inst_equations [abbreviation, in LocalComp.Typing]
inst_typing_ [definition, in LocalComp.Typing]
inst_iget_ [definition, in LocalComp.Typing]
inst_equations [abbreviation, in LocalComp.Typing]
inst_equations_ [definition, in LocalComp.Typing]
inst_typing_gscope [lemma, in LocalComp.GScope]
inst_typing_gscope_ih [lemma, in LocalComp.GScope]
inst_typing_gweak [lemma, in LocalComp.BasicMetaTheory]
inst_typing_gweak_ [lemma, in LocalComp.BasicMetaTheory]
inst_iget_gweak [lemma, in LocalComp.BasicMetaTheory]
inst_equations_gweak [lemma, in LocalComp.BasicMetaTheory]
inst_equations_gweak_ih [lemma, in LocalComp.BasicMetaTheory]
inst_typing_eweak [lemma, in LocalComp.BasicMetaTheory]
inst_typing_eweak_ [lemma, in LocalComp.BasicMetaTheory]
inst_iget_eweak [lemma, in LocalComp.BasicMetaTheory]
inst_equations_eweak [lemma, in LocalComp.BasicMetaTheory]
inst_equations_inst_ih [lemma, in LocalComp.BasicMetaTheory]
inst_inst [lemma, in LocalComp.BasicMetaTheory]
inst_get [lemma, in LocalComp.BasicMetaTheory]
inst_typing_subst [lemma, in LocalComp.BasicMetaTheory]
inst_equations_subst_ih [lemma, in LocalComp.BasicMetaTheory]
inst_typing_ren [lemma, in LocalComp.BasicMetaTheory]
inst_equations_prop [lemma, in LocalComp.BasicMetaTheory]
inst_equations_ren_ih [lemma, in LocalComp.BasicMetaTheory]
inst_instance [abbreviation, in LocalComp.Inst]
inst_typing_Forall_typed [lemma, in LocalComp.Reduction]
inst_typing_inline [lemma, in LocalComp.Inlining]
inst_equations_inline_ih [lemma, in LocalComp.Inlining]
interface [module, in LocalComp.autosubst.AST]
Inversion [library]
is_qsubst_id [constructor, in LocalComp.autosubst.AST_rasimpl]
is_qsubst_ren [constructor, in LocalComp.autosubst.AST_rasimpl]
is_qren_id [constructor, in LocalComp.autosubst.RAsimpl]
is_lam_inv [lemma, in LocalComp.Pattern]
is_lam [definition, in LocalComp.Pattern]
iwf [inductive, in LocalComp.Typing]
iwf_sind [definition, in LocalComp.Typing]
iwf_ind [definition, in LocalComp.Typing]
iwf_comp [constructor, in LocalComp.Typing]
iwf_assm [constructor, in LocalComp.Typing]
iwf_nil [constructor, in LocalComp.Typing]
iwf_gweak [lemma, in LocalComp.BasicMetaTheory]
J
joinable [definition, in LocalComp.Reduction]join_pi_inv [lemma, in LocalComp.Reduction]
join_conv [lemma, in LocalComp.Reduction]
L
length_ctx_inst [lemma, in LocalComp.BasicMetaTheory]level [definition, in LocalComp.BasicAST]
liftn [abbreviation, in LocalComp.Inst]
liftn_map_map [lemma, in LocalComp.BasicMetaTheory]
liftn_subst_instance [lemma, in LocalComp.BasicMetaTheory]
liftn_ren_instance [lemma, in LocalComp.BasicMetaTheory]
liftn_liftn [lemma, in LocalComp.BasicMetaTheory]
lift_liftn [lemma, in LocalComp.BasicMetaTheory]
lift_ren_instance [lemma, in LocalComp.BasicMetaTheory]
lift_instance [abbreviation, in LocalComp.Inst]
listify [definition, in LocalComp.BasicMetaTheory]
list_comp [definition, in LocalComp.autosubst.core]
list_id [definition, in LocalComp.autosubst.core]
list_ext [definition, in LocalComp.autosubst.core]
M
map_instance [abbreviation, in LocalComp.Inst]map_ext_All [lemma, in LocalComp.Util]
meta_conv_refl [lemma, in LocalComp.Typing]
meta_conv_trans_r [lemma, in LocalComp.Typing]
meta_conv_trans_l [lemma, in LocalComp.Typing]
meta_conv [lemma, in LocalComp.Typing]
N
not_qsubst_ren_id [constructor, in LocalComp.autosubst.AST_rasimpl]not_qren_id [constructor, in LocalComp.autosubst.RAsimpl]
no_pi_lhs [definition, in LocalComp.Reduction]
nth_error_ctx_inst [lemma, in LocalComp.BasicMetaTheory]
nth_error_Some_alt [lemma, in LocalComp.Util]
O
OnOne2 [inductive, in LocalComp.Util]OnOne2_and_Forall_l [lemma, in LocalComp.Util]
OnOne2_and_Forall2 [lemma, in LocalComp.Util]
OnOne2_impl [lemma, in LocalComp.Util]
OnOne2_refl_Forall2 [lemma, in LocalComp.Util]
OnOne2_rst_comm [lemma, in LocalComp.Util]
OnOne2_sind [definition, in LocalComp.Util]
OnOne2_ind [definition, in LocalComp.Util]
OnOne2_tl [constructor, in LocalComp.Util]
OnOne2_hd [constructor, in LocalComp.Util]
OnSome [inductive, in LocalComp.Util]
onSome [definition, in LocalComp.Util]
onSomeb [definition, in LocalComp.Util]
onSomeb_onSome [lemma, in LocalComp.Util]
onSomeT [definition, in LocalComp.Util]
onSomeT_map [lemma, in LocalComp.Util]
onSomeT_onSome [lemma, in LocalComp.Util]
onSomeT_prod [lemma, in LocalComp.Util]
onSomeT_impl [lemma, in LocalComp.Util]
onSome_onSomeT [lemma, in LocalComp.Util]
OnSome_onSome [lemma, in LocalComp.Util]
OnSome_sind [definition, in LocalComp.Util]
OnSome_ind [definition, in LocalComp.Util]
OnSome_Some [constructor, in LocalComp.Util]
OnSome_None [constructor, in LocalComp.Util]
onSome_morphism [instance, in LocalComp.Util]
onSome_map [lemma, in LocalComp.Util]
option_comp [definition, in LocalComp.autosubst.core]
option_ext [definition, in LocalComp.autosubst.core]
option_id [definition, in LocalComp.autosubst.core]
option_map [definition, in LocalComp.autosubst.core]
option_rel_rst_some_rel [lemma, in LocalComp.Util]
option_map_id_onSomeT [lemma, in LocalComp.Util]
option_map_id [lemma, in LocalComp.Util]
option_map_ext_onSomeT [lemma, in LocalComp.Util]
option_map_ext [lemma, in LocalComp.Util]
option_map_option_map [lemma, in LocalComp.Util]
option_rel_diag [lemma, in LocalComp.Util]
option_rel_map_r [lemma, in LocalComp.Util]
option_rel_flip [lemma, in LocalComp.Util]
option_rel_map_l [lemma, in LocalComp.Util]
option_rel_impl [lemma, in LocalComp.Util]
option_rel_sind [definition, in LocalComp.Util]
option_rel_ind [definition, in LocalComp.Util]
option_some [constructor, in LocalComp.Util]
option_none [constructor, in LocalComp.Util]
option_rel [inductive, in LocalComp.Util]
P
passm [constructor, in LocalComp.Pattern]pat [inductive, in LocalComp.Pattern]
Pattern [library]
pattern_rules_lhs_no_lam [lemma, in LocalComp.Pattern]
pattern_rules [definition, in LocalComp.Pattern]
pat_to_term [definition, in LocalComp.Pattern]
pat_sind [definition, in LocalComp.Pattern]
pat_rec [definition, in LocalComp.Pattern]
pat_ind [definition, in LocalComp.Pattern]
pat_rect [definition, in LocalComp.Pattern]
pointwise_forall [lemma, in LocalComp.autosubst.core]
pred [inductive, in LocalComp.Pattern]
predmax_const [constructor, in LocalComp.Pattern]
pred_max_functional [lemma, in LocalComp.Pattern]
pred_max_sind [definition, in LocalComp.Pattern]
pred_max_ind [definition, in LocalComp.Pattern]
pred_max_app [constructor, in LocalComp.Pattern]
pred_max_lam [constructor, in LocalComp.Pattern]
pred_max_Pi [constructor, in LocalComp.Pattern]
pred_max_rule [constructor, in LocalComp.Pattern]
pred_max_unfold [constructor, in LocalComp.Pattern]
pred_max_beta [constructor, in LocalComp.Pattern]
pred_max [inductive, in LocalComp.Pattern]
pred_ind_alt [lemma, in LocalComp.Pattern]
pred_sind [definition, in LocalComp.Pattern]
pred_ind [definition, in LocalComp.Pattern]
pred_const [constructor, in LocalComp.Pattern]
pred_app [constructor, in LocalComp.Pattern]
pred_lam [constructor, in LocalComp.Pattern]
pred_Pi [constructor, in LocalComp.Pattern]
pred_rule [constructor, in LocalComp.Pattern]
pred_unfold [constructor, in LocalComp.Pattern]
pred_beta [constructor, in LocalComp.Pattern]
prod_comp [definition, in LocalComp.autosubst.core]
prod_ext [definition, in LocalComp.autosubst.core]
prod_id [definition, in LocalComp.autosubst.core]
prod_map [definition, in LocalComp.autosubst.core]
Q
qatom [constructor, in LocalComp.autosubst.AST_rasimpl]qnat_atom [constructor, in LocalComp.autosubst.RAsimpl]
qren [constructor, in LocalComp.autosubst.AST_rasimpl]
qren_id_view_sind [definition, in LocalComp.autosubst.RAsimpl]
qren_id_view_rec [definition, in LocalComp.autosubst.RAsimpl]
qren_id_view_ind [definition, in LocalComp.autosubst.RAsimpl]
qren_id_view_rect [definition, in LocalComp.autosubst.RAsimpl]
qren_id_view [inductive, in LocalComp.autosubst.RAsimpl]
qren_shift [constructor, in LocalComp.autosubst.RAsimpl]
qren_id [constructor, in LocalComp.autosubst.RAsimpl]
qren_cons [constructor, in LocalComp.autosubst.RAsimpl]
qren_comp [constructor, in LocalComp.autosubst.RAsimpl]
qren_atom [constructor, in LocalComp.autosubst.RAsimpl]
qS [constructor, in LocalComp.autosubst.RAsimpl]
qsubst [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_sind [definition, in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_rec [definition, in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_ind [definition, in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_rect [definition, in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view [inductive, in LocalComp.autosubst.AST_rasimpl]
qsubst_ren [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_id [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_cons [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_rcomp [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_compr [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_comp [constructor, in LocalComp.autosubst.AST_rasimpl]
qsubst_atom [constructor, in LocalComp.autosubst.AST_rasimpl]
quoted_term_sind [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_term_rec [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_term_ind [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_term_rect [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_subst_sind [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_subst_rec [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_subst_ind [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_subst_rect [definition, in LocalComp.autosubst.AST_rasimpl]
quoted_term [inductive, in LocalComp.autosubst.AST_rasimpl]
quoted_subst [inductive, in LocalComp.autosubst.AST_rasimpl]
quoted_ren_sind [definition, in LocalComp.autosubst.RAsimpl]
quoted_ren_rec [definition, in LocalComp.autosubst.RAsimpl]
quoted_ren_ind [definition, in LocalComp.autosubst.RAsimpl]
quoted_ren_rect [definition, in LocalComp.autosubst.RAsimpl]
quoted_ren [inductive, in LocalComp.autosubst.RAsimpl]
quoted_nat_sind [definition, in LocalComp.autosubst.RAsimpl]
quoted_nat_rec [definition, in LocalComp.autosubst.RAsimpl]
quoted_nat_ind [definition, in LocalComp.autosubst.RAsimpl]
quoted_nat_rect [definition, in LocalComp.autosubst.RAsimpl]
quoted_nat [inductive, in LocalComp.autosubst.RAsimpl]
q0 [constructor, in LocalComp.autosubst.RAsimpl]
R
RAsimpl [library]Red [section, in LocalComp.Pattern]
red [definition, in LocalComp.Reduction]
Red [section, in LocalComp.Reduction]
Reduction [library]
red_pi_inv [lemma, in LocalComp.Reduction]
red_ctx_red1 [lemma, in LocalComp.Reduction]
red_ctx_sind [definition, in LocalComp.Reduction]
red_ctx_ind [definition, in LocalComp.Reduction]
red_cons [constructor, in LocalComp.Reduction]
red_nil [constructor, in LocalComp.Reduction]
red_ctx [inductive, in LocalComp.Reduction]
red_conv [lemma, in LocalComp.Reduction]
red_confluent [definition, in LocalComp.Reduction]
red_ind [lemma, in LocalComp.Reduction]
red_const [constructor, in LocalComp.Reduction]
red_app_arg [constructor, in LocalComp.Reduction]
red_app_fun [constructor, in LocalComp.Reduction]
red_lam_body [constructor, in LocalComp.Reduction]
red_lam_dom [constructor, in LocalComp.Reduction]
red_Pi_cod [constructor, in LocalComp.Reduction]
red_Pi_dom [constructor, in LocalComp.Reduction]
red_rule [constructor, in LocalComp.Reduction]
red_unfold [constructor, in LocalComp.Reduction]
red_beta [constructor, in LocalComp.Reduction]
Red.hpr [variable, in LocalComp.Pattern]
_ ⊢ _ ⇒ᵨ _ [notation, in LocalComp.Pattern]
_ ⊢ _ ⇒ _ [notation, in LocalComp.Pattern]
_ ⊢ _ ↦ _ [notation, in LocalComp.Reduction]
Red.Ξ [variable, in LocalComp.Pattern]
Red.Ξ [variable, in LocalComp.Reduction]
Red.Σ [variable, in LocalComp.Pattern]
Red.Σ [variable, in LocalComp.Reduction]
red1 [inductive, in LocalComp.Reduction]
red1_pi_inv [lemma, in LocalComp.Reduction]
red1_conv [lemma, in LocalComp.Reduction]
red1_ind_alt [lemma, in LocalComp.Reduction]
red1_sind [definition, in LocalComp.Reduction]
red1_ind [definition, in LocalComp.Reduction]
Reflexive_option_rel [instance, in LocalComp.Util]
Reflexive_Forall2 [instance, in LocalComp.Util]
Reflexive_eta [instance, in LocalComp.Util]
Reflexive_red [instance, in LocalComp.Reduction]
Reflexive_conversion [instance, in LocalComp.Reduction]
RenNotations [module, in LocalComp.autosubst.unscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in LocalComp.autosubst.unscoped]
⟨ _ ⟩ (fscope) [notation, in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
RenSimplification [record, in LocalComp.autosubst.RAsimpl]
ren_subst_instance [lemma, in LocalComp.BasicMetaTheory]
ren_ctx_inst [lemma, in LocalComp.BasicMetaTheory]
ren_ctx [definition, in LocalComp.BasicMetaTheory]
ren_instance_id_ext [lemma, in LocalComp.BasicMetaTheory]
ren_instance_id [lemma, in LocalComp.BasicMetaTheory]
ren_inst [lemma, in LocalComp.BasicMetaTheory]
ren_instance_ext [lemma, in LocalComp.BasicMetaTheory]
ren_instance_comp [lemma, in LocalComp.BasicMetaTheory]
ren_instance [abbreviation, in LocalComp.Inst]
ren1 [projection, in LocalComp.autosubst.unscoped]
Ren1 [record, in LocalComp.autosubst.unscoped]
ren1 [constructor, in LocalComp.autosubst.unscoped]
Ren1 [inductive, in LocalComp.autosubst.unscoped]
ren2 [projection, in LocalComp.autosubst.unscoped]
Ren2 [record, in LocalComp.autosubst.unscoped]
ren2 [constructor, in LocalComp.autosubst.unscoped]
Ren2 [inductive, in LocalComp.autosubst.unscoped]
ren3 [projection, in LocalComp.autosubst.unscoped]
Ren3 [record, in LocalComp.autosubst.unscoped]
ren3 [constructor, in LocalComp.autosubst.unscoped]
Ren3 [inductive, in LocalComp.autosubst.unscoped]
ren4 [projection, in LocalComp.autosubst.unscoped]
Ren4 [record, in LocalComp.autosubst.unscoped]
ren4 [constructor, in LocalComp.autosubst.unscoped]
Ren4 [inductive, in LocalComp.autosubst.unscoped]
ren5 [projection, in LocalComp.autosubst.unscoped]
Ren5 [record, in LocalComp.autosubst.unscoped]
ren5 [constructor, in LocalComp.autosubst.unscoped]
Ren5 [inductive, in LocalComp.autosubst.unscoped]
rst_step_ind [lemma, in LocalComp.Util]
rtyping [definition, in LocalComp.BasicMetaTheory]
rtyping_uprens_eq [lemma, in LocalComp.BasicMetaTheory]
rtyping_uprens [lemma, in LocalComp.BasicMetaTheory]
rtyping_add [lemma, in LocalComp.BasicMetaTheory]
rtyping_comp [lemma, in LocalComp.BasicMetaTheory]
rtyping_S [lemma, in LocalComp.BasicMetaTheory]
rtyping_up [lemma, in LocalComp.BasicMetaTheory]
rtyping_morphism [instance, in LocalComp.BasicMetaTheory]
rt_step_ind [lemma, in LocalComp.Util]
S
scons [definition, in LocalComp.autosubst.unscoped]scons_morphism2 [instance, in LocalComp.autosubst.unscoped]
scons_morphism [instance, in LocalComp.autosubst.unscoped]
scons_comp' [lemma, in LocalComp.autosubst.unscoped]
scons_eta_id' [lemma, in LocalComp.autosubst.unscoped]
scons_eta' [lemma, in LocalComp.autosubst.unscoped]
scoped [definition, in LocalComp.Typing]
scoped_instance [abbreviation, in LocalComp.Typing]
scoped_inst_closed [lemma, in LocalComp.BasicMetaTheory]
scoped_inst [lemma, in LocalComp.BasicMetaTheory]
scoped_lift [lemma, in LocalComp.BasicMetaTheory]
scoped_lift_gen [lemma, in LocalComp.BasicMetaTheory]
scoped_upwards [lemma, in LocalComp.BasicMetaTheory]
scoped_subst [lemma, in LocalComp.BasicMetaTheory]
scoped_ren [lemma, in LocalComp.BasicMetaTheory]
scoped_instance_inline [lemma, in LocalComp.Inlining]
scoped_inline [lemma, in LocalComp.Inlining]
scoped_instance_inline_ih [lemma, in LocalComp.Inlining]
shift [definition, in LocalComp.autosubst.unscoped]
some_rel_option_rel [lemma, in LocalComp.Util]
some_rel_rst_comm [lemma, in LocalComp.Util]
some_rel_sind [definition, in LocalComp.Util]
some_rel_ind [definition, in LocalComp.Util]
some_rel_some [constructor, in LocalComp.Util]
some_rel [inductive, in LocalComp.Util]
styping [inductive, in LocalComp.BasicMetaTheory]
styping_alt_equiv [lemma, in LocalComp.BasicMetaTheory]
styping_alt [definition, in LocalComp.BasicMetaTheory]
styping_one [lemma, in LocalComp.BasicMetaTheory]
styping_ids [lemma, in LocalComp.BasicMetaTheory]
styping_up [lemma, in LocalComp.BasicMetaTheory]
styping_weak [lemma, in LocalComp.BasicMetaTheory]
styping_morphism [instance, in LocalComp.BasicMetaTheory]
styping_sind [definition, in LocalComp.BasicMetaTheory]
styping_ind [definition, in LocalComp.BasicMetaTheory]
SubstNotations [module, in LocalComp.autosubst.unscoped]
SubstNotations [library]
_ [ _ ; _ ] (subst_scope) [notation, in LocalComp.autosubst.unscoped]
_ [ _ ] (subst_scope) [notation, in LocalComp.autosubst.unscoped]
SubstSimplification [record, in LocalComp.autosubst.AST_rasimpl]
subst_instance_id [lemma, in LocalComp.BasicMetaTheory]
subst_ren_instance [lemma, in LocalComp.BasicMetaTheory]
subst_instance_ext [lemma, in LocalComp.BasicMetaTheory]
subst_inst_ups [lemma, in LocalComp.BasicMetaTheory]
subst_inst_closed [lemma, in LocalComp.BasicMetaTheory]
subst_inst_scoped [lemma, in LocalComp.BasicMetaTheory]
subst_instance [abbreviation, in LocalComp.BasicMetaTheory]
subst_inst [lemma, in LocalComp.BasicMetaTheory]
subst1 [projection, in LocalComp.autosubst.unscoped]
Subst1 [record, in LocalComp.autosubst.unscoped]
subst1 [constructor, in LocalComp.autosubst.unscoped]
Subst1 [inductive, in LocalComp.autosubst.unscoped]
subst2 [projection, in LocalComp.autosubst.unscoped]
Subst2 [record, in LocalComp.autosubst.unscoped]
subst2 [constructor, in LocalComp.autosubst.unscoped]
Subst2 [inductive, in LocalComp.autosubst.unscoped]
subst3 [projection, in LocalComp.autosubst.unscoped]
Subst3 [record, in LocalComp.autosubst.unscoped]
subst3 [constructor, in LocalComp.autosubst.unscoped]
Subst3 [inductive, in LocalComp.autosubst.unscoped]
subst4 [projection, in LocalComp.autosubst.unscoped]
Subst4 [record, in LocalComp.autosubst.unscoped]
subst4 [constructor, in LocalComp.autosubst.unscoped]
Subst4 [inductive, in LocalComp.autosubst.unscoped]
subst5 [projection, in LocalComp.autosubst.unscoped]
Subst5 [record, in LocalComp.autosubst.unscoped]
subst5 [constructor, in LocalComp.autosubst.unscoped]
Subst5 [inductive, in LocalComp.autosubst.unscoped]
T
TermSimplification [record, in LocalComp.autosubst.AST_rasimpl]term_rect [lemma, in LocalComp.BasicMetaTheory]
test_qsubst_ren_id [definition, in LocalComp.autosubst.AST_rasimpl]
test_qren_id [definition, in LocalComp.autosubst.RAsimpl]
Transitive_red [instance, in LocalComp.Reduction]
triangle [lemma, in LocalComp.Pattern]
triangle_citerion [definition, in LocalComp.Pattern]
trunc [definition, in LocalComp.BasicMetaTheory]
trunc_bounds [lemma, in LocalComp.BasicMetaTheory]
type_conv [constructor, in LocalComp.Typing]
type_assm [constructor, in LocalComp.Typing]
type_const [constructor, in LocalComp.Typing]
type_app [constructor, in LocalComp.Typing]
type_lam [constructor, in LocalComp.Typing]
type_pi [constructor, in LocalComp.Typing]
type_sort [constructor, in LocalComp.Typing]
type_var [constructor, in LocalComp.Typing]
type_cons [constructor, in LocalComp.BasicMetaTheory]
type_nil [constructor, in LocalComp.BasicMetaTheory]
type_assm_inv [lemma, in LocalComp.Inversion]
type_const_inv [lemma, in LocalComp.Inversion]
type_app_inv [lemma, in LocalComp.Inversion]
type_lam_inv [lemma, in LocalComp.Inversion]
type_pi_inv [lemma, in LocalComp.Inversion]
type_sort_inv [lemma, in LocalComp.Inversion]
type_var_inv [lemma, in LocalComp.Inversion]
typing [inductive, in LocalComp.Typing]
Typing [section, in LocalComp.Typing]
Typing [library]
typing_sind [definition, in LocalComp.Typing]
typing_ind [definition, in LocalComp.Typing]
typing_gscope [lemma, in LocalComp.GScope]
typing_ind_wf [lemma, in LocalComp.BasicMetaTheory]
typing_lift_closed [lemma, in LocalComp.BasicMetaTheory]
typing_gweak [lemma, in LocalComp.BasicMetaTheory]
typing_eweak [lemma, in LocalComp.BasicMetaTheory]
typing_inst_closed [lemma, in LocalComp.BasicMetaTheory]
typing_inst [lemma, in LocalComp.BasicMetaTheory]
typing_subst [lemma, in LocalComp.BasicMetaTheory]
typing_ren [lemma, in LocalComp.BasicMetaTheory]
typing_closed [lemma, in LocalComp.BasicMetaTheory]
typing_scoped [lemma, in LocalComp.BasicMetaTheory]
typing_ind [lemma, in LocalComp.BasicMetaTheory]
typing_inline [lemma, in LocalComp.Inlining]
Typing.Equations [section, in LocalComp.Typing]
Typing.Equations.conversion [variable, in LocalComp.Typing]
_ ⊢ _ ≡ _ [notation, in LocalComp.Typing]
Typing.Inst [section, in LocalComp.Typing]
Typing.Inst.typing [variable, in LocalComp.Typing]
_ ⊢ _ : _ [notation, in LocalComp.Typing]
_ ⊢ _ : _ [notation, in LocalComp.Typing]
_ ⊢ _ ≡ _ [notation, in LocalComp.Typing]
Typing.Ξ [variable, in LocalComp.Typing]
Typing.Σ [variable, in LocalComp.Typing]
U
unquote_term [definition, in LocalComp.autosubst.AST_rasimpl]unquote_subst [definition, in LocalComp.autosubst.AST_rasimpl]
unquote_ren [definition, in LocalComp.autosubst.RAsimpl]
unquote_nat [definition, in LocalComp.autosubst.RAsimpl]
unscoped [library]
UnscopedNotations [module, in LocalComp.autosubst.unscoped]
↑ (subst_scope) [notation, in LocalComp.autosubst.unscoped]
_ .. (subst_scope) [notation, in LocalComp.autosubst.unscoped]
uprens [definition, in LocalComp.BasicMetaTheory]
uprens_above [lemma, in LocalComp.BasicMetaTheory]
uprens_below [lemma, in LocalComp.BasicMetaTheory]
ups [definition, in LocalComp.Inst]
ups_above [lemma, in LocalComp.BasicMetaTheory]
ups_below [lemma, in LocalComp.BasicMetaTheory]
up_allfv [definition, in LocalComp.autosubst.unscoped]
up_ren_ren [lemma, in LocalComp.autosubst.unscoped]
up_ren [definition, in LocalComp.autosubst.unscoped]
up_term_inline [lemma, in LocalComp.Inlining]
Util [library]
V
validity [lemma, in LocalComp.BasicMetaTheory]valid_def [lemma, in LocalComp.BasicMetaTheory]
valid_comp [lemma, in LocalComp.BasicMetaTheory]
valid_assm [lemma, in LocalComp.BasicMetaTheory]
valid_wf [lemma, in LocalComp.BasicMetaTheory]
Var [record, in LocalComp.autosubst.unscoped]
Var [inductive, in LocalComp.autosubst.unscoped]
var_zero [definition, in LocalComp.autosubst.unscoped]
W
wf [inductive, in LocalComp.Typing]wf_sind [definition, in LocalComp.Typing]
wf_ind [definition, in LocalComp.Typing]
wf_cons [constructor, in LocalComp.Typing]
wf_nil [constructor, in LocalComp.Typing]
wf_gscope [lemma, in LocalComp.GScope]
wf_rules_gweak [lemma, in LocalComp.BasicMetaTheory]
wf_gweak [lemma, in LocalComp.BasicMetaTheory]
wf_eweak [lemma, in LocalComp.BasicMetaTheory]
other
_ .. (subst_scope) [notation, in LocalComp.autosubst.SubstNotations]↑ (subst_scope) [notation, in LocalComp.autosubst.SubstNotations]
_ <[ _ ] (subst_scope) [notation, in LocalComp.autosubst.SubstNotations]
_ ⋅ _ (subst_scope) [notation, in LocalComp.autosubst.SubstNotations]
∑ _ .. _ , _ (type_scope) [notation, in LocalComp.Util]
_ ;; _ | _ ⊢ _ : _ [notation, in LocalComp.Typing]
_ ;; _ | _ ⊢ _ ≡ _ [notation, in LocalComp.Typing]
_ ;; _ | _ ⊢ _ ⇒ _ [notation, in LocalComp.Pattern]
_ ,,, _ [notation, in LocalComp.Env]
_ ,, _ [notation, in LocalComp.Env]
_ ⊑ _ [notation, in LocalComp.Env]
_ ;; _ | _ ↦* _ [notation, in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ⋈ _ [notation, in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ↮ _ [notation, in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ↦* _ [notation, in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ↦ _ [notation, in LocalComp.Reduction]
list_map [notation, in LocalComp.autosubst.core]
∙ [notation, in LocalComp.Env]
⟦ _ ⟧κ [notation, in LocalComp.Inlining]
⟦ _ ⟧R⟨ _ ⟩ [notation, in LocalComp.Inlining]
⟦ _ ⟧r⟨ _ ⟩ [notation, in LocalComp.Inlining]
⟦ _ ⟧e⟨ _ ⟩ [notation, in LocalComp.Inlining]
⟦ _ ⟧×⟨ _ ⟩ [notation, in LocalComp.Inlining]
⟦ _ ⟧*⟨ _ ⟩ [notation, in LocalComp.Inlining]
⟦ _ ⟧⟨ _ ⟩ [notation, in LocalComp.Inlining]
Notation Index
C
_ >> _ (fscope) [in LocalComp.autosubst.unscoped]_ .: _ (subst_scope) [in LocalComp.autosubst.unscoped]
_ __term (subst_scope) [in LocalComp.autosubst.AST]
_ __term (subst_scope) [in LocalComp.autosubst.AST]
var (subst_scope) [in LocalComp.autosubst.AST]
_ ⟨ _ ⟩ (subst_scope) [in LocalComp.autosubst.AST]
↑__term (subst_scope) [in LocalComp.autosubst.AST]
↑__term (subst_scope) [in LocalComp.autosubst.AST]
_ [ _ ] (subst_scope) [in LocalComp.autosubst.AST]
I
⟦ _ ⟧e [in LocalComp.Inlining]⟦ _ ⟧d [in LocalComp.Inlining]
⟦ _ ⟧R [in LocalComp.Inlining]
⟦ _ ⟧r [in LocalComp.Inlining]
⟦ _ ⟧* [in LocalComp.Inlining]
⟦ _ ⟧× [in LocalComp.Inlining]
⟦ _ ⟧ [in LocalComp.Inlining]
R
_ ⊢ _ ⇒ᵨ _ [in LocalComp.Pattern]_ ⊢ _ ⇒ _ [in LocalComp.Pattern]
_ ⊢ _ ↦ _ [in LocalComp.Reduction]
⟨ _ ; _ ⟩ (fscope) [in LocalComp.autosubst.unscoped]
⟨ _ ⟩ (fscope) [in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in LocalComp.autosubst.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in LocalComp.autosubst.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in LocalComp.autosubst.unscoped]
S
_ [ _ ; _ ] (subst_scope) [in LocalComp.autosubst.unscoped]_ [ _ ] (subst_scope) [in LocalComp.autosubst.unscoped]
T
_ ⊢ _ ≡ _ [in LocalComp.Typing]_ ⊢ _ : _ [in LocalComp.Typing]
_ ⊢ _ : _ [in LocalComp.Typing]
_ ⊢ _ ≡ _ [in LocalComp.Typing]
U
↑ (subst_scope) [in LocalComp.autosubst.unscoped]_ .. (subst_scope) [in LocalComp.autosubst.unscoped]
other
_ .. (subst_scope) [in LocalComp.autosubst.SubstNotations]↑ (subst_scope) [in LocalComp.autosubst.SubstNotations]
_ <[ _ ] (subst_scope) [in LocalComp.autosubst.SubstNotations]
_ ⋅ _ (subst_scope) [in LocalComp.autosubst.SubstNotations]
∑ _ .. _ , _ (type_scope) [in LocalComp.Util]
_ ;; _ | _ ⊢ _ : _ [in LocalComp.Typing]
_ ;; _ | _ ⊢ _ ≡ _ [in LocalComp.Typing]
_ ;; _ | _ ⊢ _ ⇒ _ [in LocalComp.Pattern]
_ ,,, _ [in LocalComp.Env]
_ ,, _ [in LocalComp.Env]
_ ⊑ _ [in LocalComp.Env]
_ ;; _ | _ ↦* _ [in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ⋈ _ [in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ↮ _ [in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ↦* _ [in LocalComp.Reduction]
_ ;; _ | _ ⊢ _ ↦ _ [in LocalComp.Reduction]
list_map [in LocalComp.autosubst.core]
∙ [in LocalComp.Env]
⟦ _ ⟧κ [in LocalComp.Inlining]
⟦ _ ⟧R⟨ _ ⟩ [in LocalComp.Inlining]
⟦ _ ⟧r⟨ _ ⟩ [in LocalComp.Inlining]
⟦ _ ⟧e⟨ _ ⟩ [in LocalComp.Inlining]
⟦ _ ⟧×⟨ _ ⟩ [in LocalComp.Inlining]
⟦ _ ⟧*⟨ _ ⟩ [in LocalComp.Inlining]
⟦ _ ⟧⟨ _ ⟩ [in LocalComp.Inlining]
Module Index
C
CombineNotations [in LocalComp.autosubst.unscoped]Core [in LocalComp.autosubst.AST]
E
Extra [in LocalComp.autosubst.AST]I
interface [in LocalComp.autosubst.AST]R
RenNotations [in LocalComp.autosubst.unscoped]S
SubstNotations [in LocalComp.autosubst.unscoped]U
UnscopedNotations [in LocalComp.autosubst.unscoped]Variable Index
I
Injectivity.hnopi [in LocalComp.Reduction]Injectivity.Ξ [in LocalComp.Reduction]
Injectivity.Σ [in LocalComp.Reduction]
Inline.hclosed [in LocalComp.Inlining]
Inline.h_type [in LocalComp.Inlining]
Inline.h_conv_unfold [in LocalComp.Inlining]
Inline.Σ [in LocalComp.Inlining]
Inline.κ [in LocalComp.Inlining]
R
Red.hpr [in LocalComp.Pattern]Red.Ξ [in LocalComp.Pattern]
Red.Ξ [in LocalComp.Reduction]
Red.Σ [in LocalComp.Pattern]
Red.Σ [in LocalComp.Reduction]
T
Typing.Equations.conversion [in LocalComp.Typing]Typing.Inst.typing [in LocalComp.Typing]
Typing.Ξ [in LocalComp.Typing]
Typing.Σ [in LocalComp.Typing]
Library Index
A
ASTAST_preamble
AST_rasimpl
B
BasicASTBasicMetaTheory
C
coreE
EnvG
GScopeI
InliningInst
Inversion
P
PatternR
RAsimplReduction
S
SubstNotationsT
TypingU
unscopedUtil
Lemma Index
A
All_map [in LocalComp.Util]All_prod [in LocalComp.Util]
All_forallb [in LocalComp.Util]
All_impl [in LocalComp.Util]
All_Forall [in LocalComp.Util]
apply_subst_sound [in LocalComp.autosubst.AST_rasimpl]
apply_ren_sound [in LocalComp.autosubst.RAsimpl]
autosubst_simpl_styping [in LocalComp.BasicMetaTheory]
autosubst_simpl_rtyping [in LocalComp.BasicMetaTheory]
autosubst_simpl_term_subst [in LocalComp.autosubst.AST_rasimpl]
autosubst_simpl_term_ren [in LocalComp.autosubst.AST_rasimpl]
C
closed_inst [in LocalComp.BasicMetaTheory]closed_lift_instance [in LocalComp.BasicMetaTheory]
closed_subst_instance [in LocalComp.BasicMetaTheory]
closed_subst [in LocalComp.BasicMetaTheory]
closed_ren_instance [in LocalComp.BasicMetaTheory]
closed_ren [in LocalComp.BasicMetaTheory]
clos_refl_sym_trans_incl [in LocalComp.Util]
cong_inst [in LocalComp.BasicMetaTheory]
conservativity [in LocalComp.Inlining]
conversion_ind [in LocalComp.BasicMetaTheory]
conv_gweak [in LocalComp.BasicMetaTheory]
conv_eweak [in LocalComp.BasicMetaTheory]
conv_insts [in LocalComp.BasicMetaTheory]
conv_inst_closed [in LocalComp.BasicMetaTheory]
conv_inst [in LocalComp.BasicMetaTheory]
conv_subst [in LocalComp.BasicMetaTheory]
conv_ren [in LocalComp.BasicMetaTheory]
conv_ctx_irr [in LocalComp.BasicMetaTheory]
conv_equiv [in LocalComp.Reduction]
conv_inline [in LocalComp.Inlining]
conv_ren_inst [in LocalComp.Inlining]
Core.congr_assm [in LocalComp.autosubst.AST]
Core.congr_const [in LocalComp.autosubst.AST]
Core.congr_app [in LocalComp.autosubst.AST]
Core.congr_lam [in LocalComp.autosubst.AST]
Core.congr_Pi [in LocalComp.autosubst.AST]
Core.congr_Sort [in LocalComp.autosubst.AST]
Core.instId'_term_pointwise [in LocalComp.autosubst.AST]
Core.instId'_term [in LocalComp.autosubst.AST]
Core.renRen_term [in LocalComp.autosubst.AST]
Core.renRen'_term_pointwise [in LocalComp.autosubst.AST]
Core.renSubst_term_pointwise [in LocalComp.autosubst.AST]
Core.renSubst_term [in LocalComp.autosubst.AST]
Core.rinstId'_term_pointwise [in LocalComp.autosubst.AST]
Core.rinstId'_term [in LocalComp.autosubst.AST]
Core.rinstInst_up_term_term [in LocalComp.autosubst.AST]
Core.rinstInst'_term_pointwise [in LocalComp.autosubst.AST]
Core.rinstInst'_term [in LocalComp.autosubst.AST]
Core.substRen_term_pointwise [in LocalComp.autosubst.AST]
Core.substRen_term [in LocalComp.autosubst.AST]
Core.substSubst_term_pointwise [in LocalComp.autosubst.AST]
Core.substSubst_term [in LocalComp.autosubst.AST]
Core.upExtRen_term_term [in LocalComp.autosubst.AST]
Core.upExt_term_term [in LocalComp.autosubst.AST]
Core.upId_term_term [in LocalComp.autosubst.AST]
Core.upRen_term_term [in LocalComp.autosubst.AST]
Core.up_subst_subst_term_term [in LocalComp.autosubst.AST]
Core.up_subst_ren_term_term [in LocalComp.autosubst.AST]
Core.up_ren_subst_term_term [in LocalComp.autosubst.AST]
Core.up_ren_ren_term_term [in LocalComp.autosubst.AST]
Core.up_term_term [in LocalComp.autosubst.AST]
Core.varLRen'_term_pointwise [in LocalComp.autosubst.AST]
Core.varLRen'_term [in LocalComp.autosubst.AST]
Core.varL'_term_pointwise [in LocalComp.autosubst.AST]
Core.varL'_term [in LocalComp.autosubst.AST]
cr_rep_inline [in LocalComp.Inlining]
cr_pat_inline [in LocalComp.Inlining]
ctx_inst_comp [in LocalComp.BasicMetaTheory]
ctx_inst_app [in LocalComp.BasicMetaTheory]
D
diamond [in LocalComp.Pattern]E
equations_typing_gscope [in LocalComp.GScope]equation_typing_gscope [in LocalComp.GScope]
equation_typing_gweak [in LocalComp.BasicMetaTheory]
equation_typing_eweak [in LocalComp.BasicMetaTheory]
equiv_const [in LocalComp.Reduction]
equiv_app [in LocalComp.Reduction]
equiv_lam [in LocalComp.Reduction]
equiv_Pi [in LocalComp.Reduction]
equiv_join [in LocalComp.Reduction]
equiv_red_ind [in LocalComp.Reduction]
eq_subst_trunc [in LocalComp.BasicMetaTheory]
eq_subst_on_up [in LocalComp.BasicMetaTheory]
eq_gscope_gcons [in LocalComp.Inlining]
eval_ren_sound [in LocalComp.autosubst.RAsimpl]
extends_gcons [in LocalComp.BasicMetaTheory]
extends_nil [in LocalComp.BasicMetaTheory]
ext_term_scoped [in LocalComp.BasicMetaTheory]
F
fold_left_ext [in LocalComp.Util]fold_left_ind [in LocalComp.Util]
fold_left_map [in LocalComp.Util]
forallb_All [in LocalComp.Util]
forall_All [in LocalComp.Util]
Forall2_rst_OnOne2 [in LocalComp.Util]
Forall2_nth_error_l [in LocalComp.Util]
Forall2_diag [in LocalComp.Util]
Forall2_map_r [in LocalComp.Util]
Forall2_map_l [in LocalComp.Util]
funcomp_assoc [in LocalComp.autosubst.core]
G
gcons_neq [in LocalComp.Inlining]gcons_eq [in LocalComp.Inlining]
gscope_apps_inv [in LocalComp.GScope]
gscope_crule_gweak [in LocalComp.BasicMetaTheory]
gscope_gweak [in LocalComp.BasicMetaTheory]
gscope_ind [in LocalComp.BasicMetaTheory]
gwf_type [in LocalComp.Inlining]
gwf_conv_unfold [in LocalComp.Inlining]
gwf_gclosed [in LocalComp.Inlining]
I
ictx_get_case [in LocalComp.BasicMetaTheory]ictx_get_weak [in LocalComp.BasicMetaTheory]
ictx_get_comp_inline [in LocalComp.Inlining]
ictx_get_assm_inline [in LocalComp.Inlining]
ictx_get_map [in LocalComp.Inlining]
iget_subst [in LocalComp.BasicMetaTheory]
iget_ren [in LocalComp.BasicMetaTheory]
inline_nil_id [in LocalComp.Inlining]
inline_ctx_ext [in LocalComp.Inlining]
inline_ictx_ext [in LocalComp.Inlining]
inline_crules_ext [in LocalComp.Inlining]
inline_crule_ext [in LocalComp.Inlining]
inline_list_ext [in LocalComp.Inlining]
inline_instance_ext [in LocalComp.Inlining]
inline_ext [in LocalComp.Inlining]
inline_ctx_inst [in LocalComp.Inlining]
inline_inst [in LocalComp.Inlining]
inline_ren_instance [in LocalComp.Inlining]
inline_iget [in LocalComp.Inlining]
inline_subst [in LocalComp.Inlining]
inline_ren [in LocalComp.Inlining]
inlining [in LocalComp.Inlining]
inst_typing_gscope [in LocalComp.GScope]
inst_typing_gscope_ih [in LocalComp.GScope]
inst_typing_gweak [in LocalComp.BasicMetaTheory]
inst_typing_gweak_ [in LocalComp.BasicMetaTheory]
inst_iget_gweak [in LocalComp.BasicMetaTheory]
inst_equations_gweak [in LocalComp.BasicMetaTheory]
inst_equations_gweak_ih [in LocalComp.BasicMetaTheory]
inst_typing_eweak [in LocalComp.BasicMetaTheory]
inst_typing_eweak_ [in LocalComp.BasicMetaTheory]
inst_iget_eweak [in LocalComp.BasicMetaTheory]
inst_equations_eweak [in LocalComp.BasicMetaTheory]
inst_equations_inst_ih [in LocalComp.BasicMetaTheory]
inst_inst [in LocalComp.BasicMetaTheory]
inst_get [in LocalComp.BasicMetaTheory]
inst_typing_subst [in LocalComp.BasicMetaTheory]
inst_equations_subst_ih [in LocalComp.BasicMetaTheory]
inst_typing_ren [in LocalComp.BasicMetaTheory]
inst_equations_prop [in LocalComp.BasicMetaTheory]
inst_equations_ren_ih [in LocalComp.BasicMetaTheory]
inst_typing_Forall_typed [in LocalComp.Reduction]
inst_typing_inline [in LocalComp.Inlining]
inst_equations_inline_ih [in LocalComp.Inlining]
is_lam_inv [in LocalComp.Pattern]
iwf_gweak [in LocalComp.BasicMetaTheory]
J
join_pi_inv [in LocalComp.Reduction]join_conv [in LocalComp.Reduction]
L
length_ctx_inst [in LocalComp.BasicMetaTheory]liftn_map_map [in LocalComp.BasicMetaTheory]
liftn_subst_instance [in LocalComp.BasicMetaTheory]
liftn_ren_instance [in LocalComp.BasicMetaTheory]
liftn_liftn [in LocalComp.BasicMetaTheory]
lift_liftn [in LocalComp.BasicMetaTheory]
lift_ren_instance [in LocalComp.BasicMetaTheory]
M
map_ext_All [in LocalComp.Util]meta_conv_refl [in LocalComp.Typing]
meta_conv_trans_r [in LocalComp.Typing]
meta_conv_trans_l [in LocalComp.Typing]
meta_conv [in LocalComp.Typing]
N
nth_error_ctx_inst [in LocalComp.BasicMetaTheory]nth_error_Some_alt [in LocalComp.Util]
O
OnOne2_and_Forall_l [in LocalComp.Util]OnOne2_and_Forall2 [in LocalComp.Util]
OnOne2_impl [in LocalComp.Util]
OnOne2_refl_Forall2 [in LocalComp.Util]
OnOne2_rst_comm [in LocalComp.Util]
onSomeb_onSome [in LocalComp.Util]
onSomeT_map [in LocalComp.Util]
onSomeT_onSome [in LocalComp.Util]
onSomeT_prod [in LocalComp.Util]
onSomeT_impl [in LocalComp.Util]
onSome_onSomeT [in LocalComp.Util]
OnSome_onSome [in LocalComp.Util]
onSome_map [in LocalComp.Util]
option_rel_rst_some_rel [in LocalComp.Util]
option_map_id_onSomeT [in LocalComp.Util]
option_map_id [in LocalComp.Util]
option_map_ext_onSomeT [in LocalComp.Util]
option_map_ext [in LocalComp.Util]
option_map_option_map [in LocalComp.Util]
option_rel_diag [in LocalComp.Util]
option_rel_map_r [in LocalComp.Util]
option_rel_flip [in LocalComp.Util]
option_rel_map_l [in LocalComp.Util]
option_rel_impl [in LocalComp.Util]
P
pattern_rules_lhs_no_lam [in LocalComp.Pattern]pointwise_forall [in LocalComp.autosubst.core]
pred_max_functional [in LocalComp.Pattern]
pred_ind_alt [in LocalComp.Pattern]
R
red_pi_inv [in LocalComp.Reduction]red_ctx_red1 [in LocalComp.Reduction]
red_conv [in LocalComp.Reduction]
red_ind [in LocalComp.Reduction]
red1_pi_inv [in LocalComp.Reduction]
red1_conv [in LocalComp.Reduction]
red1_ind_alt [in LocalComp.Reduction]
ren_subst_instance [in LocalComp.BasicMetaTheory]
ren_ctx_inst [in LocalComp.BasicMetaTheory]
ren_instance_id_ext [in LocalComp.BasicMetaTheory]
ren_instance_id [in LocalComp.BasicMetaTheory]
ren_inst [in LocalComp.BasicMetaTheory]
ren_instance_ext [in LocalComp.BasicMetaTheory]
ren_instance_comp [in LocalComp.BasicMetaTheory]
rst_step_ind [in LocalComp.Util]
rtyping_uprens_eq [in LocalComp.BasicMetaTheory]
rtyping_uprens [in LocalComp.BasicMetaTheory]
rtyping_add [in LocalComp.BasicMetaTheory]
rtyping_comp [in LocalComp.BasicMetaTheory]
rtyping_S [in LocalComp.BasicMetaTheory]
rtyping_up [in LocalComp.BasicMetaTheory]
rt_step_ind [in LocalComp.Util]
S
scons_comp' [in LocalComp.autosubst.unscoped]scons_eta_id' [in LocalComp.autosubst.unscoped]
scons_eta' [in LocalComp.autosubst.unscoped]
scoped_inst_closed [in LocalComp.BasicMetaTheory]
scoped_inst [in LocalComp.BasicMetaTheory]
scoped_lift [in LocalComp.BasicMetaTheory]
scoped_lift_gen [in LocalComp.BasicMetaTheory]
scoped_upwards [in LocalComp.BasicMetaTheory]
scoped_subst [in LocalComp.BasicMetaTheory]
scoped_ren [in LocalComp.BasicMetaTheory]
scoped_instance_inline [in LocalComp.Inlining]
scoped_inline [in LocalComp.Inlining]
scoped_instance_inline_ih [in LocalComp.Inlining]
some_rel_option_rel [in LocalComp.Util]
some_rel_rst_comm [in LocalComp.Util]
styping_alt_equiv [in LocalComp.BasicMetaTheory]
styping_one [in LocalComp.BasicMetaTheory]
styping_ids [in LocalComp.BasicMetaTheory]
styping_up [in LocalComp.BasicMetaTheory]
styping_weak [in LocalComp.BasicMetaTheory]
subst_instance_id [in LocalComp.BasicMetaTheory]
subst_ren_instance [in LocalComp.BasicMetaTheory]
subst_instance_ext [in LocalComp.BasicMetaTheory]
subst_inst_ups [in LocalComp.BasicMetaTheory]
subst_inst_closed [in LocalComp.BasicMetaTheory]
subst_inst_scoped [in LocalComp.BasicMetaTheory]
subst_inst [in LocalComp.BasicMetaTheory]
T
term_rect [in LocalComp.BasicMetaTheory]triangle [in LocalComp.Pattern]
trunc_bounds [in LocalComp.BasicMetaTheory]
type_assm_inv [in LocalComp.Inversion]
type_const_inv [in LocalComp.Inversion]
type_app_inv [in LocalComp.Inversion]
type_lam_inv [in LocalComp.Inversion]
type_pi_inv [in LocalComp.Inversion]
type_sort_inv [in LocalComp.Inversion]
type_var_inv [in LocalComp.Inversion]
typing_gscope [in LocalComp.GScope]
typing_ind_wf [in LocalComp.BasicMetaTheory]
typing_lift_closed [in LocalComp.BasicMetaTheory]
typing_gweak [in LocalComp.BasicMetaTheory]
typing_eweak [in LocalComp.BasicMetaTheory]
typing_inst_closed [in LocalComp.BasicMetaTheory]
typing_inst [in LocalComp.BasicMetaTheory]
typing_subst [in LocalComp.BasicMetaTheory]
typing_ren [in LocalComp.BasicMetaTheory]
typing_closed [in LocalComp.BasicMetaTheory]
typing_scoped [in LocalComp.BasicMetaTheory]
typing_ind [in LocalComp.BasicMetaTheory]
typing_inline [in LocalComp.Inlining]
U
uprens_above [in LocalComp.BasicMetaTheory]uprens_below [in LocalComp.BasicMetaTheory]
ups_above [in LocalComp.BasicMetaTheory]
ups_below [in LocalComp.BasicMetaTheory]
up_ren_ren [in LocalComp.autosubst.unscoped]
up_term_inline [in LocalComp.Inlining]
V
validity [in LocalComp.BasicMetaTheory]valid_def [in LocalComp.BasicMetaTheory]
valid_comp [in LocalComp.BasicMetaTheory]
valid_assm [in LocalComp.BasicMetaTheory]
valid_wf [in LocalComp.BasicMetaTheory]
W
wf_gscope [in LocalComp.GScope]wf_rules_gweak [in LocalComp.BasicMetaTheory]
wf_gweak [in LocalComp.BasicMetaTheory]
wf_eweak [in LocalComp.BasicMetaTheory]
Constructor Index
A
All_cons [in LocalComp.Util]All_nil [in LocalComp.Util]
Assm [in LocalComp.Env]
C
Comp [in LocalComp.Env]cong_const [in LocalComp.Typing]
cong_app [in LocalComp.Typing]
cong_lam [in LocalComp.Typing]
cong_Pi [in LocalComp.Typing]
conv_trans [in LocalComp.Typing]
conv_sym [in LocalComp.Typing]
conv_refl [in LocalComp.Typing]
conv_red [in LocalComp.Typing]
conv_unfold [in LocalComp.Typing]
conv_beta [in LocalComp.Typing]
Core.app [in LocalComp.autosubst.AST]
Core.assm [in LocalComp.autosubst.AST]
Core.const [in LocalComp.autosubst.AST]
Core.lam [in LocalComp.autosubst.AST]
Core.Pi [in LocalComp.autosubst.AST]
Core.Sort [in LocalComp.autosubst.AST]
Core.up_term [in LocalComp.autosubst.AST]
Core.var [in LocalComp.autosubst.AST]
D
Def [in LocalComp.Env]E
ers_other [in LocalComp.autosubst.AST_rasimpl]ers_ren_r [in LocalComp.autosubst.AST_rasimpl]
ers_cons_r [in LocalComp.autosubst.AST_rasimpl]
ers_rcomp_r [in LocalComp.autosubst.AST_rasimpl]
ers_compr_r [in LocalComp.autosubst.AST_rasimpl]
ers_comp_r [in LocalComp.autosubst.AST_rasimpl]
ers_id_r [in LocalComp.autosubst.AST_rasimpl]
ers_id_l [in LocalComp.autosubst.AST_rasimpl]
esr_other [in LocalComp.autosubst.AST_rasimpl]
esr_cons_shift [in LocalComp.autosubst.AST_rasimpl]
esr_ren_l [in LocalComp.autosubst.AST_rasimpl]
esr_cons_r [in LocalComp.autosubst.AST_rasimpl]
esr_comp_r [in LocalComp.autosubst.AST_rasimpl]
esr_id_r [in LocalComp.autosubst.AST_rasimpl]
esr_id_l [in LocalComp.autosubst.AST_rasimpl]
es_other [in LocalComp.autosubst.AST_rasimpl]
es_ren_r [in LocalComp.autosubst.AST_rasimpl]
es_ren_l [in LocalComp.autosubst.AST_rasimpl]
es_cons_r [in LocalComp.autosubst.AST_rasimpl]
es_rcomp_r [in LocalComp.autosubst.AST_rasimpl]
es_compr_r [in LocalComp.autosubst.AST_rasimpl]
es_comp_r [in LocalComp.autosubst.AST_rasimpl]
es_id_r [in LocalComp.autosubst.AST_rasimpl]
es_id_l [in LocalComp.autosubst.AST_rasimpl]
eval_ren_comp_other [in LocalComp.autosubst.RAsimpl]
eval_ren_cons_r [in LocalComp.autosubst.RAsimpl]
eval_ren_comp_r [in LocalComp.autosubst.RAsimpl]
eval_ren_cons_shift [in LocalComp.autosubst.RAsimpl]
eval_ren_id_r [in LocalComp.autosubst.RAsimpl]
eval_ren_id_l [in LocalComp.autosubst.RAsimpl]
G
gscope_assm [in LocalComp.Typing]gscope_const [in LocalComp.Typing]
gscope_app [in LocalComp.Typing]
gscope_lam [in LocalComp.Typing]
gscope_pi [in LocalComp.Typing]
gscope_sort [in LocalComp.Typing]
gscope_var [in LocalComp.Typing]
gwf_def [in LocalComp.Typing]
gwf_nil [in LocalComp.Typing]
I
ids [in LocalComp.autosubst.unscoped]is_qsubst_id [in LocalComp.autosubst.AST_rasimpl]
is_qsubst_ren [in LocalComp.autosubst.AST_rasimpl]
is_qren_id [in LocalComp.autosubst.RAsimpl]
iwf_comp [in LocalComp.Typing]
iwf_assm [in LocalComp.Typing]
iwf_nil [in LocalComp.Typing]
N
not_qsubst_ren_id [in LocalComp.autosubst.AST_rasimpl]not_qren_id [in LocalComp.autosubst.RAsimpl]
O
OnOne2_tl [in LocalComp.Util]OnOne2_hd [in LocalComp.Util]
OnSome_Some [in LocalComp.Util]
OnSome_None [in LocalComp.Util]
option_some [in LocalComp.Util]
option_none [in LocalComp.Util]
P
passm [in LocalComp.Pattern]predmax_const [in LocalComp.Pattern]
pred_max_app [in LocalComp.Pattern]
pred_max_lam [in LocalComp.Pattern]
pred_max_Pi [in LocalComp.Pattern]
pred_max_rule [in LocalComp.Pattern]
pred_max_unfold [in LocalComp.Pattern]
pred_max_beta [in LocalComp.Pattern]
pred_const [in LocalComp.Pattern]
pred_app [in LocalComp.Pattern]
pred_lam [in LocalComp.Pattern]
pred_Pi [in LocalComp.Pattern]
pred_rule [in LocalComp.Pattern]
pred_unfold [in LocalComp.Pattern]
pred_beta [in LocalComp.Pattern]
Q
qatom [in LocalComp.autosubst.AST_rasimpl]qnat_atom [in LocalComp.autosubst.RAsimpl]
qren [in LocalComp.autosubst.AST_rasimpl]
qren_shift [in LocalComp.autosubst.RAsimpl]
qren_id [in LocalComp.autosubst.RAsimpl]
qren_cons [in LocalComp.autosubst.RAsimpl]
qren_comp [in LocalComp.autosubst.RAsimpl]
qren_atom [in LocalComp.autosubst.RAsimpl]
qS [in LocalComp.autosubst.RAsimpl]
qsubst [in LocalComp.autosubst.AST_rasimpl]
qsubst_ren [in LocalComp.autosubst.AST_rasimpl]
qsubst_id [in LocalComp.autosubst.AST_rasimpl]
qsubst_cons [in LocalComp.autosubst.AST_rasimpl]
qsubst_rcomp [in LocalComp.autosubst.AST_rasimpl]
qsubst_compr [in LocalComp.autosubst.AST_rasimpl]
qsubst_comp [in LocalComp.autosubst.AST_rasimpl]
qsubst_atom [in LocalComp.autosubst.AST_rasimpl]
q0 [in LocalComp.autosubst.RAsimpl]
R
red_cons [in LocalComp.Reduction]red_nil [in LocalComp.Reduction]
red_const [in LocalComp.Reduction]
red_app_arg [in LocalComp.Reduction]
red_app_fun [in LocalComp.Reduction]
red_lam_body [in LocalComp.Reduction]
red_lam_dom [in LocalComp.Reduction]
red_Pi_cod [in LocalComp.Reduction]
red_Pi_dom [in LocalComp.Reduction]
red_rule [in LocalComp.Reduction]
red_unfold [in LocalComp.Reduction]
red_beta [in LocalComp.Reduction]
ren1 [in LocalComp.autosubst.unscoped]
ren2 [in LocalComp.autosubst.unscoped]
ren3 [in LocalComp.autosubst.unscoped]
ren4 [in LocalComp.autosubst.unscoped]
ren5 [in LocalComp.autosubst.unscoped]
S
some_rel_some [in LocalComp.Util]subst1 [in LocalComp.autosubst.unscoped]
subst2 [in LocalComp.autosubst.unscoped]
subst3 [in LocalComp.autosubst.unscoped]
subst4 [in LocalComp.autosubst.unscoped]
subst5 [in LocalComp.autosubst.unscoped]
T
type_conv [in LocalComp.Typing]type_assm [in LocalComp.Typing]
type_const [in LocalComp.Typing]
type_app [in LocalComp.Typing]
type_lam [in LocalComp.Typing]
type_pi [in LocalComp.Typing]
type_sort [in LocalComp.Typing]
type_var [in LocalComp.Typing]
type_cons [in LocalComp.BasicMetaTheory]
type_nil [in LocalComp.BasicMetaTheory]
W
wf_cons [in LocalComp.Typing]wf_nil [in LocalComp.Typing]
Inductive Index
A
All [in LocalComp.Util]C
conversion [in LocalComp.Typing]Core.term [in LocalComp.autosubst.AST]
Core.Up_term [in LocalComp.autosubst.AST]
E
eval_subst_rcomp_view [in LocalComp.autosubst.AST_rasimpl]eval_subst_compr_view [in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view [in LocalComp.autosubst.AST_rasimpl]
eval_ren_comp_view [in LocalComp.autosubst.RAsimpl]
G
gdecl [in LocalComp.Env]gscope [in LocalComp.Typing]
gwf [in LocalComp.Typing]
I
idecl [in LocalComp.Env]iwf [in LocalComp.Typing]
O
OnOne2 [in LocalComp.Util]OnSome [in LocalComp.Util]
option_rel [in LocalComp.Util]
P
pat [in LocalComp.Pattern]pred [in LocalComp.Pattern]
pred_max [in LocalComp.Pattern]
Q
qren_id_view [in LocalComp.autosubst.RAsimpl]qsubst_ren_id_view [in LocalComp.autosubst.AST_rasimpl]
quoted_term [in LocalComp.autosubst.AST_rasimpl]
quoted_subst [in LocalComp.autosubst.AST_rasimpl]
quoted_ren [in LocalComp.autosubst.RAsimpl]
quoted_nat [in LocalComp.autosubst.RAsimpl]
R
red_ctx [in LocalComp.Reduction]red1 [in LocalComp.Reduction]
Ren1 [in LocalComp.autosubst.unscoped]
Ren2 [in LocalComp.autosubst.unscoped]
Ren3 [in LocalComp.autosubst.unscoped]
Ren4 [in LocalComp.autosubst.unscoped]
Ren5 [in LocalComp.autosubst.unscoped]
S
some_rel [in LocalComp.Util]styping [in LocalComp.BasicMetaTheory]
Subst1 [in LocalComp.autosubst.unscoped]
Subst2 [in LocalComp.autosubst.unscoped]
Subst3 [in LocalComp.autosubst.unscoped]
Subst4 [in LocalComp.autosubst.unscoped]
Subst5 [in LocalComp.autosubst.unscoped]
T
typing [in LocalComp.Typing]V
Var [in LocalComp.autosubst.unscoped]W
wf [in LocalComp.Typing]Projection Index
A
autosubst_simpl_csubst [in LocalComp.autosubst.AST_rasimpl]autosubst_simpl_term [in LocalComp.autosubst.AST_rasimpl]
autosubst_simpl_ren [in LocalComp.autosubst.RAsimpl]
C
Core.up_term [in LocalComp.autosubst.AST]cr_typ [in LocalComp.Env]
cr_rep [in LocalComp.Env]
cr_sub [in LocalComp.Env]
cr_pat [in LocalComp.Env]
cr_env [in LocalComp.Env]
E
eq_typ [in LocalComp.Env]eq_rhs [in LocalComp.Env]
eq_lhs [in LocalComp.Env]
eq_env [in LocalComp.Env]
I
ids [in LocalComp.autosubst.unscoped]R
ren1 [in LocalComp.autosubst.unscoped]ren2 [in LocalComp.autosubst.unscoped]
ren3 [in LocalComp.autosubst.unscoped]
ren4 [in LocalComp.autosubst.unscoped]
ren5 [in LocalComp.autosubst.unscoped]
S
subst1 [in LocalComp.autosubst.unscoped]subst2 [in LocalComp.autosubst.unscoped]
subst3 [in LocalComp.autosubst.unscoped]
subst4 [in LocalComp.autosubst.unscoped]
subst5 [in LocalComp.autosubst.unscoped]
Section Index
I
Injectivity [in LocalComp.Reduction]Inline [in LocalComp.Inlining]
R
Red [in LocalComp.Pattern]Red [in LocalComp.Reduction]
T
Typing [in LocalComp.Typing]Typing.Equations [in LocalComp.Typing]
Typing.Inst [in LocalComp.Typing]
Instance Index
C
Core.ren_term_morphism2 [in LocalComp.autosubst.AST]Core.ren_term_morphism [in LocalComp.autosubst.AST]
Core.Ren_term [in LocalComp.autosubst.AST]
Core.subst_term_morphism2 [in LocalComp.autosubst.AST]
Core.subst_term_morphism [in LocalComp.autosubst.AST]
Core.Subst_term [in LocalComp.autosubst.AST]
Core.Up_term_term [in LocalComp.autosubst.AST]
Core.VarInstance_term [in LocalComp.autosubst.AST]
E
equiv_trans [in LocalComp.Reduction]equiv_sym [in LocalComp.Reduction]
equiv_refl [in LocalComp.Reduction]
F
funcomp_morphism2 [in LocalComp.autosubst.core]funcomp_morphism [in LocalComp.autosubst.core]
I
idsRen [in LocalComp.autosubst.unscoped]O
onSome_morphism [in LocalComp.Util]R
Reflexive_option_rel [in LocalComp.Util]Reflexive_Forall2 [in LocalComp.Util]
Reflexive_eta [in LocalComp.Util]
Reflexive_red [in LocalComp.Reduction]
Reflexive_conversion [in LocalComp.Reduction]
rtyping_morphism [in LocalComp.BasicMetaTheory]
S
scons_morphism2 [in LocalComp.autosubst.unscoped]scons_morphism [in LocalComp.autosubst.unscoped]
styping_morphism [in LocalComp.BasicMetaTheory]
T
Transitive_red [in LocalComp.Reduction]Abbreviation Index
C
closed [in LocalComp.Typing]closed_instance [in LocalComp.Typing]
G
ginst [in LocalComp.Inlining]gscope_instance [in LocalComp.Typing]
I
inst_typing [in LocalComp.Typing]inst_iget [in LocalComp.Typing]
inst_equations [in LocalComp.Typing]
inst_equations [in LocalComp.Typing]
inst_instance [in LocalComp.Inst]
L
liftn [in LocalComp.Inst]lift_instance [in LocalComp.Inst]
M
map_instance [in LocalComp.Inst]R
ren_instance [in LocalComp.Inst]S
scoped_instance [in LocalComp.Typing]subst_instance [in LocalComp.BasicMetaTheory]
Definition Index
A
All_sind [in LocalComp.Util]All_rec [in LocalComp.Util]
All_ind [in LocalComp.Util]
All_rect [in LocalComp.Util]
ap [in LocalComp.autosubst.unscoped]
apc [in LocalComp.autosubst.unscoped]
apply_subst [in LocalComp.autosubst.AST_rasimpl]
apply_ren [in LocalComp.autosubst.RAsimpl]
apps [in LocalComp.Inst]
aref [in LocalComp.BasicAST]
C
conversion_sind [in LocalComp.Typing]conversion_ind [in LocalComp.Typing]
Core.compRenRen_term [in LocalComp.autosubst.AST]
Core.compRenSubst_term [in LocalComp.autosubst.AST]
Core.compSubstRen_term [in LocalComp.autosubst.AST]
Core.compSubstSubst_term [in LocalComp.autosubst.AST]
Core.extRen_term [in LocalComp.autosubst.AST]
Core.ext_term [in LocalComp.autosubst.AST]
Core.idSubst_term [in LocalComp.autosubst.AST]
Core.ren_term [in LocalComp.autosubst.AST]
Core.rinst_inst_term [in LocalComp.autosubst.AST]
Core.subst_term [in LocalComp.autosubst.AST]
Core.term_sind [in LocalComp.autosubst.AST]
Core.term_rec [in LocalComp.autosubst.AST]
Core.term_ind [in LocalComp.autosubst.AST]
Core.term_rect [in LocalComp.autosubst.AST]
crule_eq [in LocalComp.Env]
ctx [in LocalComp.Env]
ctx_inst [in LocalComp.Inst]
D
dummy [in LocalComp.Inst]E
equation_typing [in LocalComp.Typing]equiv [in LocalComp.Reduction]
eq_subst_on [in LocalComp.BasicMetaTheory]
eq_gscope [in LocalComp.Inlining]
eval_term_sound [in LocalComp.autosubst.AST_rasimpl]
eval_subst_sound [in LocalComp.autosubst.AST_rasimpl]
eval_term [in LocalComp.autosubst.AST_rasimpl]
eval_subst [in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_c [in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_sind [in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_rec [in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_ind [in LocalComp.autosubst.AST_rasimpl]
eval_subst_rcomp_view_rect [in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_c [in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_sind [in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_rec [in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_ind [in LocalComp.autosubst.AST_rasimpl]
eval_subst_compr_view_rect [in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_c [in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_sind [in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_rec [in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_ind [in LocalComp.autosubst.AST_rasimpl]
eval_subst_comp_view_rect [in LocalComp.autosubst.AST_rasimpl]
eval_ren [in LocalComp.autosubst.RAsimpl]
eval_ren_comp_c [in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_sind [in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_rec [in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_ind [in LocalComp.autosubst.RAsimpl]
eval_ren_comp_view_rect [in LocalComp.autosubst.RAsimpl]
extends [in LocalComp.Env]
F
funcomp [in LocalComp.autosubst.core]G
gclosed [in LocalComp.Inlining]gcons [in LocalComp.Inlining]
gctx [in LocalComp.Env]
gctx_get [in LocalComp.Env]
gdecl_sind [in LocalComp.Env]
gdecl_rec [in LocalComp.Env]
gdecl_ind [in LocalComp.Env]
gdecl_rect [in LocalComp.Env]
gnil [in LocalComp.Inlining]
gref [in LocalComp.BasicAST]
gscope_crule [in LocalComp.Typing]
gscope_sind [in LocalComp.Typing]
gscope_ind [in LocalComp.Typing]
gscope_equation [in LocalComp.GScope]
gwf_sind [in LocalComp.Typing]
gwf_ind [in LocalComp.Typing]
g_type [in LocalComp.Inlining]
g_conv_unfold [in LocalComp.Inlining]
I
ictx [in LocalComp.Env]ictx_get [in LocalComp.Env]
id [in LocalComp.autosubst.unscoped]
idecl_sind [in LocalComp.Env]
idecl_rec [in LocalComp.Env]
idecl_ind [in LocalComp.Env]
idecl_rect [in LocalComp.Env]
iget [in LocalComp.Inst]
inline [in LocalComp.Inlining]
inline_gctx_ufd [in LocalComp.Inlining]
inline_idecl [in LocalComp.Inlining]
inline_crule [in LocalComp.Inlining]
inst [in LocalComp.Inst]
instance [in LocalComp.Env]
inst_typing_ [in LocalComp.Typing]
inst_iget_ [in LocalComp.Typing]
inst_equations_ [in LocalComp.Typing]
is_lam [in LocalComp.Pattern]
iwf_sind [in LocalComp.Typing]
iwf_ind [in LocalComp.Typing]
J
joinable [in LocalComp.Reduction]L
level [in LocalComp.BasicAST]listify [in LocalComp.BasicMetaTheory]
list_comp [in LocalComp.autosubst.core]
list_id [in LocalComp.autosubst.core]
list_ext [in LocalComp.autosubst.core]
N
no_pi_lhs [in LocalComp.Reduction]O
OnOne2_sind [in LocalComp.Util]OnOne2_ind [in LocalComp.Util]
onSome [in LocalComp.Util]
onSomeb [in LocalComp.Util]
onSomeT [in LocalComp.Util]
OnSome_sind [in LocalComp.Util]
OnSome_ind [in LocalComp.Util]
option_comp [in LocalComp.autosubst.core]
option_ext [in LocalComp.autosubst.core]
option_id [in LocalComp.autosubst.core]
option_map [in LocalComp.autosubst.core]
option_rel_sind [in LocalComp.Util]
option_rel_ind [in LocalComp.Util]
P
pattern_rules [in LocalComp.Pattern]pat_to_term [in LocalComp.Pattern]
pat_sind [in LocalComp.Pattern]
pat_rec [in LocalComp.Pattern]
pat_ind [in LocalComp.Pattern]
pat_rect [in LocalComp.Pattern]
pred_max_sind [in LocalComp.Pattern]
pred_max_ind [in LocalComp.Pattern]
pred_sind [in LocalComp.Pattern]
pred_ind [in LocalComp.Pattern]
prod_comp [in LocalComp.autosubst.core]
prod_ext [in LocalComp.autosubst.core]
prod_id [in LocalComp.autosubst.core]
prod_map [in LocalComp.autosubst.core]
Q
qren_id_view_sind [in LocalComp.autosubst.RAsimpl]qren_id_view_rec [in LocalComp.autosubst.RAsimpl]
qren_id_view_ind [in LocalComp.autosubst.RAsimpl]
qren_id_view_rect [in LocalComp.autosubst.RAsimpl]
qsubst_ren_id_view_sind [in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_rec [in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_ind [in LocalComp.autosubst.AST_rasimpl]
qsubst_ren_id_view_rect [in LocalComp.autosubst.AST_rasimpl]
quoted_term_sind [in LocalComp.autosubst.AST_rasimpl]
quoted_term_rec [in LocalComp.autosubst.AST_rasimpl]
quoted_term_ind [in LocalComp.autosubst.AST_rasimpl]
quoted_term_rect [in LocalComp.autosubst.AST_rasimpl]
quoted_subst_sind [in LocalComp.autosubst.AST_rasimpl]
quoted_subst_rec [in LocalComp.autosubst.AST_rasimpl]
quoted_subst_ind [in LocalComp.autosubst.AST_rasimpl]
quoted_subst_rect [in LocalComp.autosubst.AST_rasimpl]
quoted_ren_sind [in LocalComp.autosubst.RAsimpl]
quoted_ren_rec [in LocalComp.autosubst.RAsimpl]
quoted_ren_ind [in LocalComp.autosubst.RAsimpl]
quoted_ren_rect [in LocalComp.autosubst.RAsimpl]
quoted_nat_sind [in LocalComp.autosubst.RAsimpl]
quoted_nat_rec [in LocalComp.autosubst.RAsimpl]
quoted_nat_ind [in LocalComp.autosubst.RAsimpl]
quoted_nat_rect [in LocalComp.autosubst.RAsimpl]
R
red [in LocalComp.Reduction]red_ctx_sind [in LocalComp.Reduction]
red_ctx_ind [in LocalComp.Reduction]
red_confluent [in LocalComp.Reduction]
red1_sind [in LocalComp.Reduction]
red1_ind [in LocalComp.Reduction]
ren_ctx [in LocalComp.BasicMetaTheory]
rtyping [in LocalComp.BasicMetaTheory]
S
scons [in LocalComp.autosubst.unscoped]scoped [in LocalComp.Typing]
shift [in LocalComp.autosubst.unscoped]
some_rel_sind [in LocalComp.Util]
some_rel_ind [in LocalComp.Util]
styping_alt [in LocalComp.BasicMetaTheory]
styping_sind [in LocalComp.BasicMetaTheory]
styping_ind [in LocalComp.BasicMetaTheory]
T
test_qsubst_ren_id [in LocalComp.autosubst.AST_rasimpl]test_qren_id [in LocalComp.autosubst.RAsimpl]
triangle_citerion [in LocalComp.Pattern]
trunc [in LocalComp.BasicMetaTheory]
typing_sind [in LocalComp.Typing]
typing_ind [in LocalComp.Typing]
U
unquote_term [in LocalComp.autosubst.AST_rasimpl]unquote_subst [in LocalComp.autosubst.AST_rasimpl]
unquote_ren [in LocalComp.autosubst.RAsimpl]
unquote_nat [in LocalComp.autosubst.RAsimpl]
uprens [in LocalComp.BasicMetaTheory]
ups [in LocalComp.Inst]
up_allfv [in LocalComp.autosubst.unscoped]
up_ren [in LocalComp.autosubst.unscoped]
V
var_zero [in LocalComp.autosubst.unscoped]W
wf_sind [in LocalComp.Typing]wf_ind [in LocalComp.Typing]
Record Index
C
Core.Up_term [in LocalComp.autosubst.AST]crule [in LocalComp.Env]
E
equation [in LocalComp.Env]R
RenSimplification [in LocalComp.autosubst.RAsimpl]Ren1 [in LocalComp.autosubst.unscoped]
Ren2 [in LocalComp.autosubst.unscoped]
Ren3 [in LocalComp.autosubst.unscoped]
Ren4 [in LocalComp.autosubst.unscoped]
Ren5 [in LocalComp.autosubst.unscoped]
S
SubstSimplification [in LocalComp.autosubst.AST_rasimpl]Subst1 [in LocalComp.autosubst.unscoped]
Subst2 [in LocalComp.autosubst.unscoped]
Subst3 [in LocalComp.autosubst.unscoped]
Subst4 [in LocalComp.autosubst.unscoped]
Subst5 [in LocalComp.autosubst.unscoped]
T
TermSimplification [in LocalComp.autosubst.AST_rasimpl]V
Var [in LocalComp.autosubst.unscoped]| 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 | (851 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 | (59 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 | (7 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 | (18 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 | (285 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 | (145 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) |
| 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 | (24 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 | (7 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 | (25 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 | (15 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 | (190 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 | (17 entries) |
This page has been generated by coqdoc