| 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 | (1116 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 | (71 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 | (8 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 | (19 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 | (10 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 | (460 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 | (202 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 | (49 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 | (18 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 | (1 entry) |
| 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 | (61 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 | (3 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 | (196 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 | (18 entries) |
Global Index
A
ap [definition, in unscoped]apc [definition, in unscoped]
C
ce_cexp_spec [constructor, in EffHOL]ce_cexp_index [constructor, in EffHOL]
ce_cexp_type [constructor, in EffHOL]
ce_exapp_type [constructor, in EffHOL]
ce_exabs [constructor, in EffHOL]
ce_beta [constructor, in EffHOL]
ce_trans [constructor, in EffHOL]
ce_sym [constructor, in EffHOL]
ce_refl [constructor, in EffHOL]
Church_Rosser' [lemma, in EffHOL]
Church_Rosser [lemma, in EffHOL]
Church_Rosser_ptreds [lemma, in EffHOL]
Church_Rosser_ptreds' [lemma, in EffHOL]
ci_univ [constructor, in EffHOL]
ci_ref_index [constructor, in EffHOL]
ci_ref_type [constructor, in EffHOL]
ci_refb [constructor, in EffHOL]
ci_trans [constructor, in EffHOL]
ci_sym [constructor, in EffHOL]
ci_refl [constructor, in EffHOL]
cod [definition, in core_axioms]
cod_comp [definition, in core_axioms]
cod_ext [definition, in core_axioms]
cod_id [definition, in core_axioms]
cod_map [definition, in core_axioms]
CombineNotations [module, in unscoped]
_ >> _ (fscope) [notation, in unscoped]
_ .: _ (subst_scope) [notation, in unscoped]
Consistency [lemma, in EffHOL_to_HOL]
conv_arrow_inv [lemma, in EffHOL]
conv_pi_inv [lemma, in EffHOL]
conv_comp_inv [lemma, in EffHOL]
conv_type_subst [lemma, in EffHOL]
conv_exp_ren [lemma, in EffHOL]
conv_spec_ren [lemma, in EffHOL]
conv_index_ren [lemma, in EffHOL]
conv_prog_ren [lemma, in EffHOL]
conv_type_ren [lemma, in EffHOL]
conv_spec_sind [definition, in EffHOL]
conv_spec_ind [definition, in EffHOL]
conv_exp_sind [definition, in EffHOL]
conv_exp_ind [definition, in EffHOL]
conv_spec [inductive, in EffHOL]
conv_exp [inductive, in EffHOL]
conv_index_sind [definition, in EffHOL]
conv_index_ind [definition, in EffHOL]
conv_index [inductive, in EffHOL]
conv_prog_sind [definition, in EffHOL]
conv_prog_ind [definition, in EffHOL]
conv_prog [inductive, in EffHOL]
conv_type [definition, in EffHOL]
Core [module, in syntax]
core [library]
core_axioms [library]
Core.abs [constructor, in syntax]
Core.after [constructor, in syntax]
Core.all [constructor, in syntax]
Core.app [constructor, in syntax]
Core.arrow [constructor, in syntax]
Core.bind [constructor, in syntax]
Core.cexp [constructor, in syntax]
Core.comp [constructor, in syntax]
Core.compRenRen_form [definition, in syntax]
Core.compRenRen_term [definition, in syntax]
Core.compRenRen_spec [definition, in syntax]
Core.compRenRen_exp [definition, in syntax]
Core.compRenRen_index [definition, in syntax]
Core.compRenRen_prog [definition, in syntax]
Core.compRenRen_type [definition, in syntax]
Core.compRenSubst_form [definition, in syntax]
Core.compRenSubst_term [definition, in syntax]
Core.compRenSubst_spec [definition, in syntax]
Core.compRenSubst_exp [definition, in syntax]
Core.compRenSubst_index [definition, in syntax]
Core.compRenSubst_prog [definition, in syntax]
Core.compRenSubst_type [definition, in syntax]
Core.compSubstRen_form [definition, in syntax]
Core.compSubstRen_term [definition, in syntax]
Core.compSubstRen_spec [definition, in syntax]
Core.compSubstRen_exp [definition, in syntax]
Core.compSubstRen_index [definition, in syntax]
Core.compSubstRen_prog [definition, in syntax]
Core.compSubstRen_type [definition, in syntax]
Core.compSubstSubst_form [definition, in syntax]
Core.compSubstSubst_term [definition, in syntax]
Core.compSubstSubst_spec [definition, in syntax]
Core.compSubstSubst_exp [definition, in syntax]
Core.compSubstSubst_index [definition, in syntax]
Core.compSubstSubst_prog [definition, in syntax]
Core.compSubstSubst_type [definition, in syntax]
Core.congr_holds [lemma, in syntax]
Core.congr_all [lemma, in syntax]
Core.congr_implies [lemma, in syntax]
Core.congr_cterm [lemma, in syntax]
Core.congr_spall [lemma, in syntax]
Core.congr_tmall [lemma, in syntax]
Core.congr_tyall [lemma, in syntax]
Core.congr_after [lemma, in syntax]
Core.congr_spimplies [lemma, in syntax]
Core.congr_spholds [lemma, in syntax]
Core.congr_exapp [lemma, in syntax]
Core.congr_exabs [lemma, in syntax]
Core.congr_cexp [lemma, in syntax]
Core.congr_univ [lemma, in syntax]
Core.congr_ref [lemma, in syntax]
Core.congr_refb [lemma, in syntax]
Core.congr_bind [lemma, in syntax]
Core.congr_ret [lemma, in syntax]
Core.congr_tmapp [lemma, in syntax]
Core.congr_tyapp [lemma, in syntax]
Core.congr_tmabs [lemma, in syntax]
Core.congr_tyabs [lemma, in syntax]
Core.congr_comp [lemma, in syntax]
Core.congr_pi [lemma, in syntax]
Core.congr_arrow [lemma, in syntax]
Core.congr_abs [lemma, in syntax]
Core.congr_app [lemma, in syntax]
Core.cterm [constructor, in syntax]
Core.exabs [constructor, in syntax]
Core.exapp [constructor, in syntax]
Core.exp [inductive, in syntax]
Core.exp_sind [definition, in syntax]
Core.exp_rec [definition, in syntax]
Core.exp_ind [definition, in syntax]
Core.exp_rect [definition, in syntax]
Core.extRen_form [definition, in syntax]
Core.extRen_term [definition, in syntax]
Core.extRen_spec [definition, in syntax]
Core.extRen_exp [definition, in syntax]
Core.extRen_index [definition, in syntax]
Core.extRen_prog [definition, in syntax]
Core.extRen_type [definition, in syntax]
Core.ext_form [definition, in syntax]
Core.ext_term [definition, in syntax]
Core.ext_spec [definition, in syntax]
Core.ext_exp [definition, in syntax]
Core.ext_index [definition, in syntax]
Core.ext_prog [definition, in syntax]
Core.ext_type [definition, in syntax]
Core.form [inductive, in syntax]
Core.form_sind [definition, in syntax]
Core.form_rec [definition, in syntax]
Core.form_ind [definition, in syntax]
Core.form_rect [definition, in syntax]
Core.holds [constructor, in syntax]
Core.idSubst_form [definition, in syntax]
Core.idSubst_term [definition, in syntax]
Core.idSubst_spec [definition, in syntax]
Core.idSubst_exp [definition, in syntax]
Core.idSubst_index [definition, in syntax]
Core.idSubst_prog [definition, in syntax]
Core.idSubst_type [definition, in syntax]
Core.implies [constructor, in syntax]
Core.index [inductive, in syntax]
Core.index_sind [definition, in syntax]
Core.index_rec [definition, in syntax]
Core.index_ind [definition, in syntax]
Core.index_rect [definition, in syntax]
Core.instId'_form_pointwise [lemma, in syntax]
Core.instId'_form [lemma, in syntax]
Core.instId'_term_pointwise [lemma, in syntax]
Core.instId'_term [lemma, in syntax]
Core.instId'_spec_pointwise [lemma, in syntax]
Core.instId'_spec [lemma, in syntax]
Core.instId'_exp_pointwise [lemma, in syntax]
Core.instId'_exp [lemma, in syntax]
Core.instId'_index_pointwise [lemma, in syntax]
Core.instId'_index [lemma, in syntax]
Core.instId'_prog_pointwise [lemma, in syntax]
Core.instId'_prog [lemma, in syntax]
Core.instId'_type_pointwise [lemma, in syntax]
Core.instId'_type [lemma, in syntax]
Core.pi [constructor, in syntax]
Core.prog [inductive, in syntax]
Core.prog_sind [definition, in syntax]
Core.prog_rec [definition, in syntax]
Core.prog_ind [definition, in syntax]
Core.prog_rect [definition, in syntax]
Core.ref [constructor, in syntax]
Core.refb [constructor, in syntax]
Core.renRen_form [lemma, in syntax]
Core.renRen_term [lemma, in syntax]
Core.renRen_spec [lemma, in syntax]
Core.renRen_exp [lemma, in syntax]
Core.renRen_index [lemma, in syntax]
Core.renRen_prog [lemma, in syntax]
Core.renRen_type [lemma, in syntax]
Core.renRen'_form_pointwise [lemma, in syntax]
Core.renRen'_term_pointwise [lemma, in syntax]
Core.renRen'_spec_pointwise [lemma, in syntax]
Core.renRen'_exp_pointwise [lemma, in syntax]
Core.renRen'_index_pointwise [lemma, in syntax]
Core.renRen'_prog_pointwise [lemma, in syntax]
Core.renRen'_type_pointwise [lemma, in syntax]
Core.renSubst_form_pointwise [lemma, in syntax]
Core.renSubst_form [lemma, in syntax]
Core.renSubst_term_pointwise [lemma, in syntax]
Core.renSubst_term [lemma, in syntax]
Core.renSubst_spec_pointwise [lemma, in syntax]
Core.renSubst_spec [lemma, in syntax]
Core.renSubst_exp_pointwise [lemma, in syntax]
Core.renSubst_exp [lemma, in syntax]
Core.renSubst_index_pointwise [lemma, in syntax]
Core.renSubst_index [lemma, in syntax]
Core.renSubst_prog_pointwise [lemma, in syntax]
Core.renSubst_prog [lemma, in syntax]
Core.renSubst_type_pointwise [lemma, in syntax]
Core.renSubst_type [lemma, in syntax]
Core.ren_type_morphism2 [instance, in syntax]
Core.ren_type_morphism [instance, in syntax]
Core.ren_prog_morphism2 [instance, in syntax]
Core.ren_prog_morphism [instance, in syntax]
Core.ren_index_morphism2 [instance, in syntax]
Core.ren_index_morphism [instance, in syntax]
Core.ren_exp_morphism2 [instance, in syntax]
Core.ren_exp_morphism [instance, in syntax]
Core.ren_spec_morphism2 [instance, in syntax]
Core.ren_spec_morphism [instance, in syntax]
Core.ren_term_morphism2 [instance, in syntax]
Core.ren_term_morphism [instance, in syntax]
Core.ren_form_morphism2 [instance, in syntax]
Core.ren_form_morphism [instance, in syntax]
Core.Ren_type [instance, in syntax]
Core.Ren_prog [instance, in syntax]
Core.Ren_index [instance, in syntax]
Core.Ren_exp [instance, in syntax]
Core.Ren_spec [instance, in syntax]
Core.Ren_term [instance, in syntax]
Core.Ren_form [instance, in syntax]
Core.ren_form [definition, in syntax]
Core.ren_term [definition, in syntax]
Core.ren_spec [definition, in syntax]
Core.ren_exp [definition, in syntax]
Core.ren_index [definition, in syntax]
Core.ren_prog [definition, in syntax]
Core.ren_type [definition, in syntax]
Core.ret [constructor, in syntax]
Core.rinstId'_form_pointwise [lemma, in syntax]
Core.rinstId'_form [lemma, in syntax]
Core.rinstId'_term_pointwise [lemma, in syntax]
Core.rinstId'_term [lemma, in syntax]
Core.rinstId'_spec_pointwise [lemma, in syntax]
Core.rinstId'_spec [lemma, in syntax]
Core.rinstId'_exp_pointwise [lemma, in syntax]
Core.rinstId'_exp [lemma, in syntax]
Core.rinstId'_index_pointwise [lemma, in syntax]
Core.rinstId'_index [lemma, in syntax]
Core.rinstId'_prog_pointwise [lemma, in syntax]
Core.rinstId'_prog [lemma, in syntax]
Core.rinstId'_type_pointwise [lemma, in syntax]
Core.rinstId'_type [lemma, in syntax]
Core.rinstInst_up_term_term [lemma, in syntax]
Core.rinstInst_up_exp_exp [lemma, in syntax]
Core.rinstInst_up_exp_prog [lemma, in syntax]
Core.rinstInst_up_exp_type [lemma, in syntax]
Core.rinstInst_up_prog_exp [lemma, in syntax]
Core.rinstInst_up_type_exp [lemma, in syntax]
Core.rinstInst_up_prog_prog [lemma, in syntax]
Core.rinstInst_up_prog_type [lemma, in syntax]
Core.rinstInst_up_type_prog [lemma, in syntax]
Core.rinstInst_up_type_type [lemma, in syntax]
Core.rinstInst'_form_pointwise [lemma, in syntax]
Core.rinstInst'_form [lemma, in syntax]
Core.rinstInst'_term_pointwise [lemma, in syntax]
Core.rinstInst'_term [lemma, in syntax]
Core.rinstInst'_spec_pointwise [lemma, in syntax]
Core.rinstInst'_spec [lemma, in syntax]
Core.rinstInst'_exp_pointwise [lemma, in syntax]
Core.rinstInst'_exp [lemma, in syntax]
Core.rinstInst'_index_pointwise [lemma, in syntax]
Core.rinstInst'_index [lemma, in syntax]
Core.rinstInst'_prog_pointwise [lemma, in syntax]
Core.rinstInst'_prog [lemma, in syntax]
Core.rinstInst'_type_pointwise [lemma, in syntax]
Core.rinstInst'_type [lemma, in syntax]
Core.rinst_inst_form [definition, in syntax]
Core.rinst_inst_term [definition, in syntax]
Core.rinst_inst_spec [definition, in syntax]
Core.rinst_inst_exp [definition, in syntax]
Core.rinst_inst_index [definition, in syntax]
Core.rinst_inst_prog [definition, in syntax]
Core.rinst_inst_type [definition, in syntax]
Core.spall [constructor, in syntax]
Core.spec [inductive, in syntax]
Core.spec_sind [definition, in syntax]
Core.spec_rec [definition, in syntax]
Core.spec_ind [definition, in syntax]
Core.spec_rect [definition, in syntax]
Core.spholds [constructor, in syntax]
Core.spimplies [constructor, in syntax]
Core.substRen_form_pointwise [lemma, in syntax]
Core.substRen_form [lemma, in syntax]
Core.substRen_term_pointwise [lemma, in syntax]
Core.substRen_term [lemma, in syntax]
Core.substRen_spec_pointwise [lemma, in syntax]
Core.substRen_spec [lemma, in syntax]
Core.substRen_exp_pointwise [lemma, in syntax]
Core.substRen_exp [lemma, in syntax]
Core.substRen_index_pointwise [lemma, in syntax]
Core.substRen_index [lemma, in syntax]
Core.substRen_prog_pointwise [lemma, in syntax]
Core.substRen_prog [lemma, in syntax]
Core.substRen_type_pointwise [lemma, in syntax]
Core.substRen_type [lemma, in syntax]
Core.substSubst_form_pointwise [lemma, in syntax]
Core.substSubst_form [lemma, in syntax]
Core.substSubst_term_pointwise [lemma, in syntax]
Core.substSubst_term [lemma, in syntax]
Core.substSubst_spec_pointwise [lemma, in syntax]
Core.substSubst_spec [lemma, in syntax]
Core.substSubst_exp_pointwise [lemma, in syntax]
Core.substSubst_exp [lemma, in syntax]
Core.substSubst_index_pointwise [lemma, in syntax]
Core.substSubst_index [lemma, in syntax]
Core.substSubst_prog_pointwise [lemma, in syntax]
Core.substSubst_prog [lemma, in syntax]
Core.substSubst_type_pointwise [lemma, in syntax]
Core.substSubst_type [lemma, in syntax]
Core.subst_type_morphism2 [instance, in syntax]
Core.subst_type_morphism [instance, in syntax]
Core.subst_prog_morphism2 [instance, in syntax]
Core.subst_prog_morphism [instance, in syntax]
Core.subst_index_morphism2 [instance, in syntax]
Core.subst_index_morphism [instance, in syntax]
Core.subst_exp_morphism2 [instance, in syntax]
Core.subst_exp_morphism [instance, in syntax]
Core.subst_spec_morphism2 [instance, in syntax]
Core.subst_spec_morphism [instance, in syntax]
Core.subst_term_morphism2 [instance, in syntax]
Core.subst_term_morphism [instance, in syntax]
Core.subst_form_morphism2 [instance, in syntax]
Core.subst_form_morphism [instance, in syntax]
Core.Subst_type [instance, in syntax]
Core.Subst_prog [instance, in syntax]
Core.Subst_index [instance, in syntax]
Core.Subst_exp [instance, in syntax]
Core.Subst_spec [instance, in syntax]
Core.Subst_term [instance, in syntax]
Core.Subst_form [instance, in syntax]
Core.subst_form [definition, in syntax]
Core.subst_term [definition, in syntax]
Core.subst_spec [definition, in syntax]
Core.subst_exp [definition, in syntax]
Core.subst_index [definition, in syntax]
Core.subst_prog [definition, in syntax]
Core.subst_type [definition, in syntax]
Core.term [inductive, in syntax]
Core.term_sind [definition, in syntax]
Core.term_rec [definition, in syntax]
Core.term_ind [definition, in syntax]
Core.term_rect [definition, in syntax]
Core.tmabs [constructor, in syntax]
Core.tmall [constructor, in syntax]
Core.tmapp [constructor, in syntax]
Core.tyabs [constructor, in syntax]
Core.tyall [constructor, in syntax]
Core.tyapp [constructor, in syntax]
Core.type [inductive, in syntax]
Core.type_sind [definition, in syntax]
Core.type_rec [definition, in syntax]
Core.type_ind [definition, in syntax]
Core.type_rect [definition, in syntax]
Core.univ [constructor, in syntax]
Core.upExtRen_term_term [lemma, in syntax]
Core.upExtRen_exp_exp [lemma, in syntax]
Core.upExtRen_exp_prog [lemma, in syntax]
Core.upExtRen_exp_type [lemma, in syntax]
Core.upExtRen_prog_exp [lemma, in syntax]
Core.upExtRen_type_exp [lemma, in syntax]
Core.upExtRen_prog_prog [lemma, in syntax]
Core.upExtRen_prog_type [lemma, in syntax]
Core.upExtRen_type_prog [lemma, in syntax]
Core.upExtRen_type_type [lemma, in syntax]
Core.upExt_term_term [lemma, in syntax]
Core.upExt_exp_exp [lemma, in syntax]
Core.upExt_exp_prog [lemma, in syntax]
Core.upExt_exp_type [lemma, in syntax]
Core.upExt_prog_exp [lemma, in syntax]
Core.upExt_type_exp [lemma, in syntax]
Core.upExt_prog_prog [lemma, in syntax]
Core.upExt_prog_type [lemma, in syntax]
Core.upExt_type_prog [lemma, in syntax]
Core.upExt_type_type [lemma, in syntax]
Core.upId_term_term [lemma, in syntax]
Core.upId_exp_exp [lemma, in syntax]
Core.upId_exp_prog [lemma, in syntax]
Core.upId_exp_type [lemma, in syntax]
Core.upId_prog_exp [lemma, in syntax]
Core.upId_type_exp [lemma, in syntax]
Core.upId_prog_prog [lemma, in syntax]
Core.upId_prog_type [lemma, in syntax]
Core.upId_type_prog [lemma, in syntax]
Core.upId_type_type [lemma, in syntax]
Core.upRen_term_term [lemma, in syntax]
Core.upRen_exp_exp [lemma, in syntax]
Core.upRen_exp_prog [lemma, in syntax]
Core.upRen_exp_type [lemma, in syntax]
Core.upRen_prog_exp [lemma, in syntax]
Core.upRen_type_exp [lemma, in syntax]
Core.upRen_prog_prog [lemma, in syntax]
Core.upRen_prog_type [lemma, in syntax]
Core.upRen_type_prog [lemma, in syntax]
Core.upRen_type_type [lemma, in syntax]
Core.Up_type_type [instance, in syntax]
Core.Up_type_prog [instance, in syntax]
Core.Up_prog_type [instance, in syntax]
Core.Up_prog_prog [instance, in syntax]
Core.Up_type_exp [instance, in syntax]
Core.Up_prog_exp [instance, in syntax]
Core.Up_exp_type [instance, in syntax]
Core.Up_exp_prog [instance, in syntax]
Core.Up_exp_exp [instance, in syntax]
Core.Up_term_term [instance, in syntax]
Core.up_type [projection, in syntax]
Core.Up_type [record, in syntax]
Core.up_type [constructor, in syntax]
Core.Up_type [inductive, in syntax]
Core.up_prog [projection, in syntax]
Core.Up_prog [record, in syntax]
Core.up_prog [constructor, in syntax]
Core.Up_prog [inductive, in syntax]
Core.up_index [projection, in syntax]
Core.Up_index [record, in syntax]
Core.up_index [constructor, in syntax]
Core.Up_index [inductive, in syntax]
Core.up_exp [projection, in syntax]
Core.Up_exp [record, in syntax]
Core.up_exp [constructor, in syntax]
Core.Up_exp [inductive, in syntax]
Core.up_spec [projection, in syntax]
Core.Up_spec [record, in syntax]
Core.up_spec [constructor, in syntax]
Core.Up_spec [inductive, in syntax]
Core.up_term [projection, in syntax]
Core.Up_term [record, in syntax]
Core.up_term [constructor, in syntax]
Core.Up_term [inductive, in syntax]
Core.up_form [projection, in syntax]
Core.Up_form [record, in syntax]
Core.up_form [constructor, in syntax]
Core.Up_form [inductive, in syntax]
Core.up_subst_subst_term_term [lemma, in syntax]
Core.up_subst_ren_term_term [lemma, in syntax]
Core.up_ren_subst_term_term [lemma, in syntax]
Core.up_ren_ren_term_term [lemma, in syntax]
Core.up_term_term [lemma, in syntax]
Core.up_subst_subst_exp_exp [lemma, in syntax]
Core.up_subst_subst_exp_prog [lemma, in syntax]
Core.up_subst_subst_exp_type [lemma, in syntax]
Core.up_subst_subst_prog_exp [lemma, in syntax]
Core.up_subst_subst_type_exp [lemma, in syntax]
Core.up_subst_ren_exp_exp [lemma, in syntax]
Core.up_subst_ren_exp_prog [lemma, in syntax]
Core.up_subst_ren_exp_type [lemma, in syntax]
Core.up_subst_ren_prog_exp [lemma, in syntax]
Core.up_subst_ren_type_exp [lemma, in syntax]
Core.up_ren_subst_exp_exp [lemma, in syntax]
Core.up_ren_subst_exp_prog [lemma, in syntax]
Core.up_ren_subst_exp_type [lemma, in syntax]
Core.up_ren_subst_prog_exp [lemma, in syntax]
Core.up_ren_subst_type_exp [lemma, in syntax]
Core.up_ren_ren_exp_exp [lemma, in syntax]
Core.up_ren_ren_exp_prog [lemma, in syntax]
Core.up_ren_ren_exp_type [lemma, in syntax]
Core.up_ren_ren_prog_exp [lemma, in syntax]
Core.up_ren_ren_type_exp [lemma, in syntax]
Core.up_exp_exp [lemma, in syntax]
Core.up_exp_prog [lemma, in syntax]
Core.up_exp_type [lemma, in syntax]
Core.up_prog_exp [lemma, in syntax]
Core.up_type_exp [lemma, in syntax]
Core.up_subst_subst_prog_prog [lemma, in syntax]
Core.up_subst_subst_prog_type [lemma, in syntax]
Core.up_subst_subst_type_prog [lemma, in syntax]
Core.up_subst_ren_prog_prog [lemma, in syntax]
Core.up_subst_ren_prog_type [lemma, in syntax]
Core.up_subst_ren_type_prog [lemma, in syntax]
Core.up_ren_subst_prog_prog [lemma, in syntax]
Core.up_ren_subst_prog_type [lemma, in syntax]
Core.up_ren_subst_type_prog [lemma, in syntax]
Core.up_ren_ren_prog_prog [lemma, in syntax]
Core.up_ren_ren_prog_type [lemma, in syntax]
Core.up_ren_ren_type_prog [lemma, in syntax]
Core.up_prog_prog [lemma, in syntax]
Core.up_prog_type [lemma, in syntax]
Core.up_type_prog [lemma, in syntax]
Core.up_subst_subst_type_type [lemma, in syntax]
Core.up_subst_ren_type_type [lemma, in syntax]
Core.up_ren_subst_type_type [lemma, in syntax]
Core.up_ren_ren_type_type [lemma, in syntax]
Core.up_type_type [lemma, in syntax]
Core.VarInstance_type [instance, in syntax]
Core.VarInstance_prog [instance, in syntax]
Core.VarInstance_exp [instance, in syntax]
Core.VarInstance_term [instance, in syntax]
Core.varLRen'_term_pointwise [lemma, in syntax]
Core.varLRen'_term [lemma, in syntax]
Core.varLRen'_exp_pointwise [lemma, in syntax]
Core.varLRen'_exp [lemma, in syntax]
Core.varLRen'_prog_pointwise [lemma, in syntax]
Core.varLRen'_prog [lemma, in syntax]
Core.varLRen'_type_pointwise [lemma, in syntax]
Core.varLRen'_type [lemma, in syntax]
Core.varL'_term_pointwise [lemma, in syntax]
Core.varL'_term [lemma, in syntax]
Core.varL'_exp_pointwise [lemma, in syntax]
Core.varL'_exp [lemma, in syntax]
Core.varL'_prog_pointwise [lemma, in syntax]
Core.varL'_prog [lemma, in syntax]
Core.varL'_type_pointwise [lemma, in syntax]
Core.varL'_type [lemma, in syntax]
Core.var_term [constructor, in syntax]
Core.var_exp [constructor, in syntax]
Core.var_prog [constructor, in syntax]
Core.var_type [constructor, in syntax]
[ _ ] (fscope) [notation, in syntax]
[ _ ; _ ] (fscope) [notation, in syntax]
[ _ ] (fscope) [notation, in syntax]
[ _ ; _ ; _ ] (fscope) [notation, in syntax]
[ _ ; _ ; _ ] (fscope) [notation, in syntax]
[ _ ] (fscope) [notation, in syntax]
[ _ ] (fscope) [notation, in syntax]
⟨ _ ⟩ (fscope) [notation, in syntax]
⟨ _ ; _ ⟩ (fscope) [notation, in syntax]
⟨ _ ⟩ (fscope) [notation, in syntax]
⟨ _ ; _ ; _ ⟩ (fscope) [notation, in syntax]
⟨ _ ; _ ; _ ⟩ (fscope) [notation, in syntax]
⟨ _ ⟩ (fscope) [notation, in syntax]
⟨ _ ⟩ (fscope) [notation, in syntax]
_ __type (subst_scope) [notation, in syntax]
_ __type (subst_scope) [notation, in syntax]
var (subst_scope) [notation, in syntax]
_ ⟨ _ ⟩ (subst_scope) [notation, in syntax]
↑__type (subst_scope) [notation, in syntax]
↑__type (subst_scope) [notation, in syntax]
_ [ _ ] (subst_scope) [notation, in syntax]
_ __prog (subst_scope) [notation, in syntax]
_ __prog (subst_scope) [notation, in syntax]
var (subst_scope) [notation, in syntax]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in syntax]
↑__prog (subst_scope) [notation, in syntax]
↑__type (subst_scope) [notation, in syntax]
↑__prog (subst_scope) [notation, in syntax]
↑__prog (subst_scope) [notation, in syntax]
_ [ _ ; _ ] (subst_scope) [notation, in syntax]
_ ⟨ _ ⟩ (subst_scope) [notation, in syntax]
↑__index (subst_scope) [notation, in syntax]
_ [ _ ] (subst_scope) [notation, in syntax]
_ __exp (subst_scope) [notation, in syntax]
_ __exp (subst_scope) [notation, in syntax]
var (subst_scope) [notation, in syntax]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in syntax]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in syntax]
↑__exp (subst_scope) [notation, in syntax]
↑__exp (subst_scope) [notation, in syntax]
↑__type (subst_scope) [notation, in syntax]
↑__prog (subst_scope) [notation, in syntax]
↑__exp (subst_scope) [notation, in syntax]
↑__exp (subst_scope) [notation, in syntax]
_ [ _ ; _ ; _ ] (subst_scope) [notation, in syntax]
↑__spec (subst_scope) [notation, in syntax]
_ [ _ ; _ ; _ ] (subst_scope) [notation, in syntax]
_ __term (subst_scope) [notation, in syntax]
_ __term (subst_scope) [notation, in syntax]
var (subst_scope) [notation, in syntax]
_ ⟨ _ ⟩ (subst_scope) [notation, in syntax]
_ ⟨ _ ⟩ (subst_scope) [notation, in syntax]
↑__term (subst_scope) [notation, in syntax]
↑__term (subst_scope) [notation, in syntax]
_ [ _ ] (subst_scope) [notation, in syntax]
↑__form (subst_scope) [notation, in syntax]
_ [ _ ] (subst_scope) [notation, in syntax]
cp_tyapp [constructor, in EffHOL]
cp_trans [constructor, in EffHOL]
cp_sym [constructor, in EffHOL]
cp_refl [constructor, in EffHOL]
cs_holds_exp2 [constructor, in EffHOL]
cs_holds_exp1 [constructor, in EffHOL]
cs_holds_prog [constructor, in EffHOL]
cs_spall_spec [constructor, in EffHOL]
cs_spall_index [constructor, in EffHOL]
cs_tmall_spec [constructor, in EffHOL]
cs_tmall_type [constructor, in EffHOL]
cs_tyall [constructor, in EffHOL]
cs_after_spec [constructor, in EffHOL]
cs_after_prog [constructor, in EffHOL]
cs_implies2 [constructor, in EffHOL]
cs_implies1 [constructor, in EffHOL]
cs_trans [constructor, in EffHOL]
cs_sym [constructor, in EffHOL]
cs_refl [constructor, in EffHOL]
ct_trans [constructor, in EffHOL]
ct_refl [constructor, in EffHOL]
ct_tred [constructor, in EffHOL]
ct_comp [constructor, in EffHOL]
ct_pi [constructor, in EffHOL]
ct_arrow2 [constructor, in EffHOL]
ct_arrow1 [constructor, in EffHOL]
ct_app2 [constructor, in EffHOL]
ct_app1 [constructor, in EffHOL]
ct_abs [constructor, in EffHOL]
ct_beta [constructor, in EffHOL]
D
Diamond_ptred [lemma, in EffHOL]E
EffHOL [library]EffHOL_to_Fw [library]
EffHOL_to_HOL [library]
Extra [module, in syntax]
F
Fext [module, in syntax]Fext.instId_form [lemma, in syntax]
Fext.instId_term [lemma, in syntax]
Fext.instId_spec [lemma, in syntax]
Fext.instId_exp [lemma, in syntax]
Fext.instId_index [lemma, in syntax]
Fext.instId_prog [lemma, in syntax]
Fext.instId_type [lemma, in syntax]
Fext.renRen'_form [lemma, in syntax]
Fext.renRen'_term [lemma, in syntax]
Fext.renRen'_spec [lemma, in syntax]
Fext.renRen'_exp [lemma, in syntax]
Fext.renRen'_index [lemma, in syntax]
Fext.renRen'_prog [lemma, in syntax]
Fext.renRen'_type [lemma, in syntax]
Fext.renSubst'_form [lemma, in syntax]
Fext.renSubst'_term [lemma, in syntax]
Fext.renSubst'_spec [lemma, in syntax]
Fext.renSubst'_exp [lemma, in syntax]
Fext.renSubst'_index [lemma, in syntax]
Fext.renSubst'_prog [lemma, in syntax]
Fext.renSubst'_type [lemma, in syntax]
Fext.rinstId_form [lemma, in syntax]
Fext.rinstId_term [lemma, in syntax]
Fext.rinstId_spec [lemma, in syntax]
Fext.rinstId_exp [lemma, in syntax]
Fext.rinstId_index [lemma, in syntax]
Fext.rinstId_prog [lemma, in syntax]
Fext.rinstId_type [lemma, in syntax]
Fext.rinstInst_form [lemma, in syntax]
Fext.rinstInst_term [lemma, in syntax]
Fext.rinstInst_spec [lemma, in syntax]
Fext.rinstInst_exp [lemma, in syntax]
Fext.rinstInst_index [lemma, in syntax]
Fext.rinstInst_prog [lemma, in syntax]
Fext.rinstInst_type [lemma, in syntax]
Fext.substRen'_form [lemma, in syntax]
Fext.substRen'_term [lemma, in syntax]
Fext.substRen'_spec [lemma, in syntax]
Fext.substRen'_exp [lemma, in syntax]
Fext.substRen'_index [lemma, in syntax]
Fext.substRen'_prog [lemma, in syntax]
Fext.substRen'_type [lemma, in syntax]
Fext.substSubst'_form [lemma, in syntax]
Fext.substSubst'_term [lemma, in syntax]
Fext.substSubst'_spec [lemma, in syntax]
Fext.substSubst'_exp [lemma, in syntax]
Fext.substSubst'_index [lemma, in syntax]
Fext.substSubst'_prog [lemma, in syntax]
Fext.substSubst'_type [lemma, in syntax]
Fext.varLRen_term [lemma, in syntax]
Fext.varLRen_exp [lemma, in syntax]
Fext.varLRen_prog [lemma, in syntax]
Fext.varLRen_type [lemma, in syntax]
Fext.varL_term [lemma, in syntax]
Fext.varL_exp [lemma, in syntax]
Fext.varL_prog [lemma, in syntax]
Fext.varL_type [lemma, in syntax]
funcomp [definition, in core]
funcomp_morphism2 [instance, in core]
funcomp_morphism [instance, in core]
funcomp_assoc [lemma, in core]
Fw [section, in EffHOL_to_Fw]
Fw_prv_sind [definition, in EffHOL_to_Fw]
Fw_prv_ind [definition, in EffHOL_to_Fw]
Fw_CONV [constructor, in EffHOL_to_Fw]
Fw_RED [constructor, in EffHOL_to_Fw]
Fw_CE [constructor, in EffHOL_to_Fw]
Fw_CI [constructor, in EffHOL_to_Fw]
Fw_SAE [constructor, in EffHOL_to_Fw]
Fw_SAI [constructor, in EffHOL_to_Fw]
Fw_EAE [constructor, in EffHOL_to_Fw]
Fw_EAI [constructor, in EffHOL_to_Fw]
Fw_TAE [constructor, in EffHOL_to_Fw]
Fw_TAI [constructor, in EffHOL_to_Fw]
Fw_IE [constructor, in EffHOL_to_Fw]
Fw_II [constructor, in EffHOL_to_Fw]
Fw_CTX [constructor, in EffHOL_to_Fw]
Fw_prv [inductive, in EffHOL_to_Fw]
Fw.iafter [variable, in EffHOL_to_Fw]
Fw.iafter_mono [variable, in EffHOL_to_Fw]
Fw.iafter_bind [variable, in EffHOL_to_Fw]
Fw.iafter_ret [variable, in EffHOL_to_Fw]
Fw.iafter_is_spec [variable, in EffHOL_to_Fw]
Fw.iafter_subst [variable, in EffHOL_to_Fw]
Fw.iafter_conv_spec [variable, in EffHOL_to_Fw]
Fw.iafter_conv_prog [variable, in EffHOL_to_Fw]
Fw.ibind [variable, in EffHOL_to_Fw]
Fw.ibind_has_type [variable, in EffHOL_to_Fw]
Fw.ibind_subst [variable, in EffHOL_to_Fw]
Fw.icomp [variable, in EffHOL_to_Fw]
Fw.icomp_has_kind [variable, in EffHOL_to_Fw]
Fw.icomp_subst [variable, in EffHOL_to_Fw]
Fw.icomp_tred [variable, in EffHOL_to_Fw]
Fw.iret [variable, in EffHOL_to_Fw]
Fw.iret_has_type [variable, in EffHOL_to_Fw]
Fw.iret_subst [variable, in EffHOL_to_Fw]
Fw.iret_red_prog [variable, in EffHOL_to_Fw]
H
has_sort_unique [lemma, in HOL]has_sort_subst' [lemma, in HOL]
has_sort_ren' [lemma, in HOL]
has_sort_subst [lemma, in HOL]
has_sort_ren [lemma, in HOL]
has_sort_sind [definition, in HOL]
has_sort_ind [definition, in HOL]
has_sort [inductive, in HOL]
has_type_subst' [lemma, in EffHOL]
has_type_subst [lemma, in EffHOL]
has_kind_subst [lemma, in EffHOL]
has_index_ren [lemma, in EffHOL]
has_type_ren [lemma, in EffHOL]
has_kind_ren [lemma, in EffHOL]
has_type_weak [lemma, in EffHOL]
has_kind_weak [lemma, in EffHOL]
has_index_sind [definition, in EffHOL]
has_index_ind [definition, in EffHOL]
has_index [inductive, in EffHOL]
has_type_sind [definition, in EffHOL]
has_type_ind [definition, in EffHOL]
has_type [inductive, in EffHOL]
has_kind_sind [definition, in EffHOL]
has_kind_ind [definition, in EffHOL]
has_kind [inductive, in EffHOL]
has_indexFw_sind [definition, in EffHOL_to_Fw]
has_indexFw_ind [definition, in EffHOL_to_Fw]
has_indexFw [inductive, in EffHOL_to_Fw]
has_typeFw_sind [definition, in EffHOL_to_Fw]
has_typeFw_ind [definition, in EffHOL_to_Fw]
has_typeFw [inductive, in EffHOL_to_Fw]
hi_conv [constructor, in EffHOL]
hi_exapp [constructor, in EffHOL]
hi_exabs [constructor, in EffHOL]
hi_cexp [constructor, in EffHOL]
hi_var [constructor, in EffHOL]
hi_conv [constructor, in EffHOL_to_Fw]
hi_exapp [constructor, in EffHOL_to_Fw]
hi_exabs [constructor, in EffHOL_to_Fw]
hi_cexp [constructor, in EffHOL_to_Fw]
hi_var [constructor, in EffHOL_to_Fw]
hk_comp [constructor, in EffHOL]
hk_pi [constructor, in EffHOL]
hk_arrow [constructor, in EffHOL]
hk_abs [constructor, in EffHOL]
hk_app [constructor, in EffHOL]
hk_var [constructor, in EffHOL]
HOL [library]
HOL_weak [lemma, in HOL]
HOL_prv_sind [definition, in HOL]
HOL_prv_ind [definition, in HOL]
HOL_CE [constructor, in HOL]
HOL_CI [constructor, in HOL]
HOL_AE [constructor, in HOL]
HOL_AI [constructor, in HOL]
HOL_IE [constructor, in HOL]
HOL_II [constructor, in HOL]
HOL_CTX [constructor, in HOL]
HOL_prv [inductive, in HOL]
HOL_to_EffHOL [library]
HOPL_HOL [lemma, in EffHOL_to_HOL]
HOPL_ren [lemma, in EffHOL]
HOPL_eq [lemma, in EffHOL]
HOPL_weak [lemma, in EffHOL]
HOPL_prv_sind [definition, in EffHOL]
HOPL_prv_ind [definition, in EffHOL]
HOPL_CONV [constructor, in EffHOL]
HOPL_RED [constructor, in EffHOL]
HOPL_MM [constructor, in EffHOL]
HOPL_ME [constructor, in EffHOL]
HOPL_MI [constructor, in EffHOL]
HOPL_CE [constructor, in EffHOL]
HOPL_CI [constructor, in EffHOL]
HOPL_SAE [constructor, in EffHOL]
HOPL_SAI [constructor, in EffHOL]
HOPL_EAE [constructor, in EffHOL]
HOPL_EAI [constructor, in EffHOL]
HOPL_TAE [constructor, in EffHOL]
HOPL_TAI [constructor, in EffHOL]
HOPL_IE [constructor, in EffHOL]
HOPL_II [constructor, in EffHOL]
HOPL_CTX [constructor, in EffHOL]
HOPL_prv [inductive, in EffHOL]
HOPL_Fw [lemma, in EffHOL_to_Fw]
hs_cterm [constructor, in HOL]
hs_var [constructor, in HOL]
ht_tmabs_inv [lemma, in EffHOL]
ht_tmabs_inv' [lemma, in EffHOL]
ht_tyabs_inv [lemma, in EffHOL]
ht_tyabs_inv' [lemma, in EffHOL]
ht_ret_inv [lemma, in EffHOL]
ht_ret_inv' [lemma, in EffHOL]
ht_conv [constructor, in EffHOL]
ht_tmapp [constructor, in EffHOL]
ht_tyapp [constructor, in EffHOL]
ht_bind [constructor, in EffHOL]
ht_ret [constructor, in EffHOL]
ht_tmabs [constructor, in EffHOL]
ht_tyabs [constructor, in EffHOL]
ht_var [constructor, in EffHOL]
ht_conv [constructor, in EffHOL_to_Fw]
ht_tmapp [constructor, in EffHOL_to_Fw]
ht_tyapp [constructor, in EffHOL_to_Fw]
ht_tmabs [constructor, in EffHOL_to_Fw]
ht_tyabs [constructor, in EffHOL_to_Fw]
ht_var [constructor, in EffHOL_to_Fw]
I
id [definition, in unscoped]ids [projection, in unscoped]
ids [constructor, in unscoped]
idsRen [instance, in unscoped]
ii_univ [constructor, in EffHOL]
ii_ref [constructor, in EffHOL]
ii_refb [constructor, in EffHOL]
interface [module, in syntax]
ip_holds [constructor, in HOL]
ip_all [constructor, in HOL]
ip_implies [constructor, in HOL]
is_prop_subst' [lemma, in HOL]
is_prop_ren' [lemma, in HOL]
is_prop_subst [lemma, in HOL]
is_prop_ren [lemma, in HOL]
is_prop_sind [definition, in HOL]
is_prop_ind [definition, in HOL]
is_prop [inductive, in HOL]
is_spec_ren' [lemma, in EffHOL]
is_spec_ren [lemma, in EffHOL]
is_index_ren [lemma, in EffHOL]
is_spec_sind [definition, in EffHOL]
is_spec_ind [definition, in EffHOL]
is_holds [constructor, in EffHOL]
is_spall [constructor, in EffHOL]
is_tmall [constructor, in EffHOL]
is_tyall [constructor, in EffHOL]
is_after [constructor, in EffHOL]
is_implies [constructor, in EffHOL]
is_spec [inductive, in EffHOL]
is_index_sind [definition, in EffHOL]
is_index_ind [definition, in EffHOL]
is_index [inductive, in EffHOL]
is_value_ren [lemma, in EffHOL]
is_value_sind [definition, in EffHOL]
is_value_ind [definition, in EffHOL]
is_value [inductive, in EffHOL]
is_specFw_sind [definition, in EffHOL_to_Fw]
is_specFw_ind [definition, in EffHOL_to_Fw]
is_holds [constructor, in EffHOL_to_Fw]
is_spall [constructor, in EffHOL_to_Fw]
is_tmall [constructor, in EffHOL_to_Fw]
is_tyall [constructor, in EffHOL_to_Fw]
is_implies [constructor, in EffHOL_to_Fw]
is_specFw [inductive, in EffHOL_to_Fw]
iv_tmabs [constructor, in EffHOL]
iv_tyabs [constructor, in EffHOL]
iv_var [constructor, in EffHOL]
K
kind [definition, in EffHOL]L
list_comp [definition, in core]list_id [definition, in core]
list_ext [definition, in core]
lup [abbreviation, in HOL]
lup [abbreviation, in EffHOL]
lup [abbreviation, in EffHOL_to_Fw]
lup_app [lemma, in EffHOL]
lup_map_el [lemma, in EffHOL]
M
maxred [definition, in EffHOL]maxred_ptred [lemma, in EffHOL]
O
option_comp [definition, in core]option_ext [definition, in core]
option_id [definition, in core]
option_map [definition, in core]
P
pointwise_forall [lemma, in core]prod_comp [definition, in core]
prod_ext [definition, in core]
prod_id [definition, in core]
prod_map [definition, in core]
ptred [inductive, in EffHOL]
ptreds [inductive, in EffHOL]
ptreds_treds [lemma, in EffHOL]
ptreds_sind [definition, in EffHOL]
ptreds_ind [definition, in EffHOL]
ptred_subst' [lemma, in EffHOL]
ptred_subst [lemma, in EffHOL]
ptred_ren [lemma, in EffHOL]
ptred_refl [lemma, in EffHOL]
ptred_treds [lemma, in EffHOL]
ptred_sind [definition, in EffHOL]
ptred_ind [definition, in EffHOL]
pt_trans [constructor, in EffHOL]
pt_ptred [constructor, in EffHOL]
pt_comp [constructor, in EffHOL]
pt_pi [constructor, in EffHOL]
pt_arrow [constructor, in EffHOL]
pt_app [constructor, in EffHOL]
pt_abs [constructor, in EffHOL]
pt_beta [constructor, in EffHOL]
pt_var [constructor, in EffHOL]
R
red_has_type [lemma, in EffHOL]red_prog_ren [lemma, in EffHOL]
red_prog_sind [definition, in EffHOL]
red_prog_ind [definition, in EffHOL]
red_prog [inductive, in EffHOL]
RenNotations [module, in unscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in unscoped]
⟨ _ ⟩ (fscope) [notation, in unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in unscoped]
ren1 [projection, in unscoped]
Ren1 [record, in unscoped]
ren1 [constructor, in unscoped]
Ren1 [inductive, in unscoped]
ren2 [projection, in unscoped]
Ren2 [record, in unscoped]
ren2 [constructor, in unscoped]
Ren2 [inductive, in unscoped]
ren3 [projection, in unscoped]
Ren3 [record, in unscoped]
ren3 [constructor, in unscoped]
Ren3 [inductive, in unscoped]
ren4 [projection, in unscoped]
Ren4 [record, in unscoped]
ren4 [constructor, in unscoped]
Ren4 [inductive, in unscoped]
ren5 [projection, in unscoped]
Ren5 [record, in unscoped]
ren5 [constructor, in unscoped]
Ren5 [inductive, in unscoped]
rp_ret [constructor, in EffHOL]
rp_betatm [constructor, in EffHOL]
rp_betaty [constructor, in EffHOL]
S
scons [definition, in unscoped]scons_morphism2 [instance, in unscoped]
scons_morphism [instance, in unscoped]
scons_comp' [lemma, in unscoped]
scons_eta_id' [lemma, in unscoped]
scons_eta' [lemma, in unscoped]
scons_comp [lemma, in unscoped_axioms]
scons_eta [lemma, in unscoped_axioms]
scons_eta_id [lemma, in unscoped_axioms]
shift [definition, in unscoped]
sort [definition, in HOL]
soundness [lemma, in HOL_to_EffHOL]
soundness_Fw [lemma, in EffHOL_to_Fw]
soundness_typing_check [lemma, in HOL_to_EffHOL]
SubstNotations [module, in unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in unscoped]
_ [ _ ] (subst_scope) [notation, in unscoped]
subst1 [projection, in unscoped]
Subst1 [record, in unscoped]
subst1 [constructor, in unscoped]
Subst1 [inductive, in unscoped]
subst2 [projection, in unscoped]
Subst2 [record, in unscoped]
subst2 [constructor, in unscoped]
Subst2 [inductive, in unscoped]
subst3 [projection, in unscoped]
Subst3 [record, in unscoped]
subst3 [constructor, in unscoped]
Subst3 [inductive, in unscoped]
subst4 [projection, in unscoped]
Subst4 [record, in unscoped]
subst4 [constructor, in unscoped]
Subst4 [inductive, in unscoped]
subst5 [projection, in unscoped]
Subst5 [record, in unscoped]
subst5 [constructor, in unscoped]
Subst5 [inductive, in unscoped]
swap [definition, in EffHOL]
syntax [library]
T
THOL_is_prop [lemma, in HOL]THOL_weak [lemma, in HOL]
THOL_prv_sind [definition, in HOL]
THOL_prv_ind [definition, in HOL]
THOL_CE [constructor, in HOL]
THOL_CI [constructor, in HOL]
THOL_AE [constructor, in HOL]
THOL_AI [constructor, in HOL]
THOL_IE [constructor, in HOL]
THOL_II [constructor, in HOL]
THOL_CTX [constructor, in HOL]
THOL_prv [inductive, in HOL]
transFw_exp_conv [lemma, in EffHOL_to_Fw]
transFw_spec_conv [lemma, in EffHOL_to_Fw]
transFw_prog_conv [lemma, in EffHOL_to_Fw]
transFw_prog_red [lemma, in EffHOL_to_Fw]
transFw_prog_is_value [lemma, in EffHOL_to_Fw]
transFw_exp_subst [lemma, in EffHOL_to_Fw]
transFw_spec_subst [lemma, in EffHOL_to_Fw]
transFw_spec_ren_ctx [lemma, in EffHOL_to_Fw]
transFw_exp_ren [lemma, in EffHOL_to_Fw]
transFw_spec_ren [lemma, in EffHOL_to_Fw]
transFw_prog_subst [lemma, in EffHOL_to_Fw]
transFw_prog_ren [lemma, in EffHOL_to_Fw]
transFw_exp_has_index [lemma, in EffHOL_to_Fw]
transFw_spec_is_spec [lemma, in EffHOL_to_Fw]
transFw_index_ren_ctx [lemma, in EffHOL_to_Fw]
transFw_index_conv [lemma, in EffHOL_to_Fw]
transFw_index_ren [lemma, in EffHOL_to_Fw]
transFw_index_subst [lemma, in EffHOL_to_Fw]
transFw_exp [definition, in EffHOL_to_Fw]
transFw_spec [definition, in EffHOL_to_Fw]
transFw_index_is_index [lemma, in EffHOL_to_Fw]
transFw_index [definition, in EffHOL_to_Fw]
transFw_prog_has_type [lemma, in EffHOL_to_Fw]
transFw_type_conv [lemma, in EffHOL_to_Fw]
transFw_type_tred [lemma, in EffHOL_to_Fw]
transFw_type_subst [lemma, in EffHOL_to_Fw]
transFw_type_ren_ctx [lemma, in EffHOL_to_Fw]
transFw_type_ren [lemma, in EffHOL_to_Fw]
transFw_prog [definition, in EffHOL_to_Fw]
transFw_type_has_kind [lemma, in EffHOL_to_Fw]
transFw_type [definition, in EffHOL_to_Fw]
trans_term_conv [lemma, in EffHOL_to_HOL]
trans_form_conv [lemma, in EffHOL_to_HOL]
trans_term_point [lemma, in EffHOL_to_HOL]
trans_form_subst' [lemma, in EffHOL_to_HOL]
trans_term_subst [lemma, in EffHOL_to_HOL]
trans_form_subst [lemma, in EffHOL_to_HOL]
trans_form_ren' [lemma, in EffHOL_to_HOL]
trans_term_ren' [lemma, in EffHOL_to_HOL]
trans_term_ren [lemma, in EffHOL_to_HOL]
trans_form_ren [lemma, in EffHOL_to_HOL]
trans_term_has_sort [lemma, in EffHOL_to_HOL]
trans_form_is_prop [lemma, in EffHOL_to_HOL]
trans_sort_conv [lemma, in EffHOL_to_HOL]
trans_sort_subst [lemma, in EffHOL_to_HOL]
trans_sort_ren [lemma, in EffHOL_to_HOL]
trans_term [definition, in EffHOL_to_HOL]
trans_form [definition, in EffHOL_to_HOL]
trans_sort [definition, in EffHOL_to_HOL]
trans_SL' [definition, in EffHOL_to_Fw]
trans_S' [definition, in EffHOL_to_Fw]
trans_T' [definition, in EffHOL_to_Fw]
trans_SL_up [lemma, in HOL_to_EffHOL]
trans_SL_lup [lemma, in HOL_to_EffHOL]
trans_SL_lup' [lemma, in HOL_to_EffHOL]
trans_is_spec [lemma, in HOL_to_EffHOL]
trans_IL_up [lemma, in HOL_to_EffHOL]
trans_IL_lup [lemma, in HOL_to_EffHOL]
trans_IL_lup' [lemma, in HOL_to_EffHOL]
trans_I_inj [lemma, in HOL_to_EffHOL]
trans_IL_el [lemma, in HOL_to_EffHOL]
trans_IL_length [lemma, in HOL_to_EffHOL]
trans_has_kind [lemma, in HOL_to_EffHOL]
trans_is_index [lemma, in HOL_to_EffHOL]
trans_SL_ren [lemma, in HOL_to_EffHOL]
trans_SL_ren' [lemma, in HOL_to_EffHOL]
trans_S_subst_spec [lemma, in HOL_to_EffHOL]
trans_S_subst' [lemma, in HOL_to_EffHOL]
trans_S_subst [lemma, in HOL_to_EffHOL]
trans_S_ren [lemma, in HOL_to_EffHOL]
trans_T_subst [lemma, in HOL_to_EffHOL]
trans_T_ren [lemma, in HOL_to_EffHOL]
trans_I_ren [lemma, in HOL_to_EffHOL]
trans_I_subst [lemma, in HOL_to_EffHOL]
trans_SL [definition, in HOL_to_EffHOL]
trans_SL' [definition, in HOL_to_EffHOL]
trans_IL [definition, in HOL_to_EffHOL]
trans_IL' [definition, in HOL_to_EffHOL]
trans_S [definition, in HOL_to_EffHOL]
trans_T [definition, in HOL_to_EffHOL]
trans_I [definition, in HOL_to_EffHOL]
treds_arrow_inv [lemma, in EffHOL]
treds_arrow_inv' [lemma, in EffHOL]
treds_pi_inv [lemma, in EffHOL]
treds_pi_inv' [lemma, in EffHOL]
treds_comp_inv [lemma, in EffHOL]
treds_comp_inv' [lemma, in EffHOL]
treds_conv [lemma, in EffHOL]
treds_ptreds [lemma, in EffHOL]
treds_comp [lemma, in EffHOL]
treds_pi [lemma, in EffHOL]
treds_abs [lemma, in EffHOL]
treds_arrow2 [lemma, in EffHOL]
treds_arrow1 [lemma, in EffHOL]
treds_app2 [lemma, in EffHOL]
treds_app1 [lemma, in EffHOL]
treds_type_trans [lemma, in EffHOL]
treds_type_sind [definition, in EffHOL]
treds_type_ind [definition, in EffHOL]
treds_type [inductive, in EffHOL]
tred_ptred [lemma, in EffHOL]
tred_type_subst [lemma, in EffHOL]
tred_type_ren [lemma, in EffHOL]
tred_type_sind [definition, in EffHOL]
tred_type_ind [definition, in EffHOL]
tred_type [inductive, in EffHOL]
ttrans_has_index [lemma, in HOL_to_EffHOL]
ttrans_has_kind [lemma, in HOL_to_EffHOL]
ttrans_E_subst_exp [lemma, in HOL_to_EffHOL]
ttrans_E_subst [lemma, in HOL_to_EffHOL]
ttrans_E_ren [lemma, in HOL_to_EffHOL]
ttrans_T_subst [lemma, in HOL_to_EffHOL]
ttrans_T_ren [lemma, in HOL_to_EffHOL]
ttrans_E [definition, in HOL_to_EffHOL]
ttrans_T [definition, in HOL_to_EffHOL]
U
unscoped [library]UnscopedNotations [module, in unscoped]
↑ (subst_scope) [notation, in unscoped]
_ .. (subst_scope) [notation, in unscoped]
unscoped_axioms [library]
up_allfv [definition, in unscoped]
up_ren_ren [lemma, in unscoped]
up_ren [definition, in unscoped]
V
Var [record, in unscoped]Var [inductive, in unscoped]
var_zero [definition, in unscoped]
other
list_map [notation, in core]Notation Index
C
_ >> _ (fscope) [in unscoped]_ .: _ (subst_scope) [in unscoped]
[ _ ] (fscope) [in syntax]
[ _ ; _ ] (fscope) [in syntax]
[ _ ] (fscope) [in syntax]
[ _ ; _ ; _ ] (fscope) [in syntax]
[ _ ; _ ; _ ] (fscope) [in syntax]
[ _ ] (fscope) [in syntax]
[ _ ] (fscope) [in syntax]
⟨ _ ⟩ (fscope) [in syntax]
⟨ _ ; _ ⟩ (fscope) [in syntax]
⟨ _ ⟩ (fscope) [in syntax]
⟨ _ ; _ ; _ ⟩ (fscope) [in syntax]
⟨ _ ; _ ; _ ⟩ (fscope) [in syntax]
⟨ _ ⟩ (fscope) [in syntax]
⟨ _ ⟩ (fscope) [in syntax]
_ __type (subst_scope) [in syntax]
_ __type (subst_scope) [in syntax]
var (subst_scope) [in syntax]
_ ⟨ _ ⟩ (subst_scope) [in syntax]
↑__type (subst_scope) [in syntax]
↑__type (subst_scope) [in syntax]
_ [ _ ] (subst_scope) [in syntax]
_ __prog (subst_scope) [in syntax]
_ __prog (subst_scope) [in syntax]
var (subst_scope) [in syntax]
_ ⟨ _ ; _ ⟩ (subst_scope) [in syntax]
↑__prog (subst_scope) [in syntax]
↑__type (subst_scope) [in syntax]
↑__prog (subst_scope) [in syntax]
↑__prog (subst_scope) [in syntax]
_ [ _ ; _ ] (subst_scope) [in syntax]
_ ⟨ _ ⟩ (subst_scope) [in syntax]
↑__index (subst_scope) [in syntax]
_ [ _ ] (subst_scope) [in syntax]
_ __exp (subst_scope) [in syntax]
_ __exp (subst_scope) [in syntax]
var (subst_scope) [in syntax]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in syntax]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in syntax]
↑__exp (subst_scope) [in syntax]
↑__exp (subst_scope) [in syntax]
↑__type (subst_scope) [in syntax]
↑__prog (subst_scope) [in syntax]
↑__exp (subst_scope) [in syntax]
↑__exp (subst_scope) [in syntax]
_ [ _ ; _ ; _ ] (subst_scope) [in syntax]
↑__spec (subst_scope) [in syntax]
_ [ _ ; _ ; _ ] (subst_scope) [in syntax]
_ __term (subst_scope) [in syntax]
_ __term (subst_scope) [in syntax]
var (subst_scope) [in syntax]
_ ⟨ _ ⟩ (subst_scope) [in syntax]
_ ⟨ _ ⟩ (subst_scope) [in syntax]
↑__term (subst_scope) [in syntax]
↑__term (subst_scope) [in syntax]
_ [ _ ] (subst_scope) [in syntax]
↑__form (subst_scope) [in syntax]
_ [ _ ] (subst_scope) [in syntax]
R
⟨ _ ; _ ⟩ (fscope) [in unscoped]⟨ _ ⟩ (fscope) [in unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ⟩ (subst_scope) [in unscoped]
S
_ [ _ ; _ ] (subst_scope) [in unscoped]_ [ _ ] (subst_scope) [in unscoped]
U
↑ (subst_scope) [in unscoped]_ .. (subst_scope) [in unscoped]
other
list_map [in core]Module Index
C
CombineNotations [in unscoped]Core [in syntax]
E
Extra [in syntax]F
Fext [in syntax]I
interface [in syntax]R
RenNotations [in unscoped]S
SubstNotations [in unscoped]U
UnscopedNotations [in unscoped]Variable Index
F
Fw.iafter [in EffHOL_to_Fw]Fw.iafter_mono [in EffHOL_to_Fw]
Fw.iafter_bind [in EffHOL_to_Fw]
Fw.iafter_ret [in EffHOL_to_Fw]
Fw.iafter_is_spec [in EffHOL_to_Fw]
Fw.iafter_subst [in EffHOL_to_Fw]
Fw.iafter_conv_spec [in EffHOL_to_Fw]
Fw.iafter_conv_prog [in EffHOL_to_Fw]
Fw.ibind [in EffHOL_to_Fw]
Fw.ibind_has_type [in EffHOL_to_Fw]
Fw.ibind_subst [in EffHOL_to_Fw]
Fw.icomp [in EffHOL_to_Fw]
Fw.icomp_has_kind [in EffHOL_to_Fw]
Fw.icomp_subst [in EffHOL_to_Fw]
Fw.icomp_tred [in EffHOL_to_Fw]
Fw.iret [in EffHOL_to_Fw]
Fw.iret_has_type [in EffHOL_to_Fw]
Fw.iret_subst [in EffHOL_to_Fw]
Fw.iret_red_prog [in EffHOL_to_Fw]
Library Index
C
corecore_axioms
E
EffHOLEffHOL_to_Fw
EffHOL_to_HOL
H
HOLHOL_to_EffHOL
S
syntaxU
unscopedunscoped_axioms
Lemma Index
C
Church_Rosser' [in EffHOL]Church_Rosser [in EffHOL]
Church_Rosser_ptreds [in EffHOL]
Church_Rosser_ptreds' [in EffHOL]
Consistency [in EffHOL_to_HOL]
conv_arrow_inv [in EffHOL]
conv_pi_inv [in EffHOL]
conv_comp_inv [in EffHOL]
conv_type_subst [in EffHOL]
conv_exp_ren [in EffHOL]
conv_spec_ren [in EffHOL]
conv_index_ren [in EffHOL]
conv_prog_ren [in EffHOL]
conv_type_ren [in EffHOL]
Core.congr_holds [in syntax]
Core.congr_all [in syntax]
Core.congr_implies [in syntax]
Core.congr_cterm [in syntax]
Core.congr_spall [in syntax]
Core.congr_tmall [in syntax]
Core.congr_tyall [in syntax]
Core.congr_after [in syntax]
Core.congr_spimplies [in syntax]
Core.congr_spholds [in syntax]
Core.congr_exapp [in syntax]
Core.congr_exabs [in syntax]
Core.congr_cexp [in syntax]
Core.congr_univ [in syntax]
Core.congr_ref [in syntax]
Core.congr_refb [in syntax]
Core.congr_bind [in syntax]
Core.congr_ret [in syntax]
Core.congr_tmapp [in syntax]
Core.congr_tyapp [in syntax]
Core.congr_tmabs [in syntax]
Core.congr_tyabs [in syntax]
Core.congr_comp [in syntax]
Core.congr_pi [in syntax]
Core.congr_arrow [in syntax]
Core.congr_abs [in syntax]
Core.congr_app [in syntax]
Core.instId'_form_pointwise [in syntax]
Core.instId'_form [in syntax]
Core.instId'_term_pointwise [in syntax]
Core.instId'_term [in syntax]
Core.instId'_spec_pointwise [in syntax]
Core.instId'_spec [in syntax]
Core.instId'_exp_pointwise [in syntax]
Core.instId'_exp [in syntax]
Core.instId'_index_pointwise [in syntax]
Core.instId'_index [in syntax]
Core.instId'_prog_pointwise [in syntax]
Core.instId'_prog [in syntax]
Core.instId'_type_pointwise [in syntax]
Core.instId'_type [in syntax]
Core.renRen_form [in syntax]
Core.renRen_term [in syntax]
Core.renRen_spec [in syntax]
Core.renRen_exp [in syntax]
Core.renRen_index [in syntax]
Core.renRen_prog [in syntax]
Core.renRen_type [in syntax]
Core.renRen'_form_pointwise [in syntax]
Core.renRen'_term_pointwise [in syntax]
Core.renRen'_spec_pointwise [in syntax]
Core.renRen'_exp_pointwise [in syntax]
Core.renRen'_index_pointwise [in syntax]
Core.renRen'_prog_pointwise [in syntax]
Core.renRen'_type_pointwise [in syntax]
Core.renSubst_form_pointwise [in syntax]
Core.renSubst_form [in syntax]
Core.renSubst_term_pointwise [in syntax]
Core.renSubst_term [in syntax]
Core.renSubst_spec_pointwise [in syntax]
Core.renSubst_spec [in syntax]
Core.renSubst_exp_pointwise [in syntax]
Core.renSubst_exp [in syntax]
Core.renSubst_index_pointwise [in syntax]
Core.renSubst_index [in syntax]
Core.renSubst_prog_pointwise [in syntax]
Core.renSubst_prog [in syntax]
Core.renSubst_type_pointwise [in syntax]
Core.renSubst_type [in syntax]
Core.rinstId'_form_pointwise [in syntax]
Core.rinstId'_form [in syntax]
Core.rinstId'_term_pointwise [in syntax]
Core.rinstId'_term [in syntax]
Core.rinstId'_spec_pointwise [in syntax]
Core.rinstId'_spec [in syntax]
Core.rinstId'_exp_pointwise [in syntax]
Core.rinstId'_exp [in syntax]
Core.rinstId'_index_pointwise [in syntax]
Core.rinstId'_index [in syntax]
Core.rinstId'_prog_pointwise [in syntax]
Core.rinstId'_prog [in syntax]
Core.rinstId'_type_pointwise [in syntax]
Core.rinstId'_type [in syntax]
Core.rinstInst_up_term_term [in syntax]
Core.rinstInst_up_exp_exp [in syntax]
Core.rinstInst_up_exp_prog [in syntax]
Core.rinstInst_up_exp_type [in syntax]
Core.rinstInst_up_prog_exp [in syntax]
Core.rinstInst_up_type_exp [in syntax]
Core.rinstInst_up_prog_prog [in syntax]
Core.rinstInst_up_prog_type [in syntax]
Core.rinstInst_up_type_prog [in syntax]
Core.rinstInst_up_type_type [in syntax]
Core.rinstInst'_form_pointwise [in syntax]
Core.rinstInst'_form [in syntax]
Core.rinstInst'_term_pointwise [in syntax]
Core.rinstInst'_term [in syntax]
Core.rinstInst'_spec_pointwise [in syntax]
Core.rinstInst'_spec [in syntax]
Core.rinstInst'_exp_pointwise [in syntax]
Core.rinstInst'_exp [in syntax]
Core.rinstInst'_index_pointwise [in syntax]
Core.rinstInst'_index [in syntax]
Core.rinstInst'_prog_pointwise [in syntax]
Core.rinstInst'_prog [in syntax]
Core.rinstInst'_type_pointwise [in syntax]
Core.rinstInst'_type [in syntax]
Core.substRen_form_pointwise [in syntax]
Core.substRen_form [in syntax]
Core.substRen_term_pointwise [in syntax]
Core.substRen_term [in syntax]
Core.substRen_spec_pointwise [in syntax]
Core.substRen_spec [in syntax]
Core.substRen_exp_pointwise [in syntax]
Core.substRen_exp [in syntax]
Core.substRen_index_pointwise [in syntax]
Core.substRen_index [in syntax]
Core.substRen_prog_pointwise [in syntax]
Core.substRen_prog [in syntax]
Core.substRen_type_pointwise [in syntax]
Core.substRen_type [in syntax]
Core.substSubst_form_pointwise [in syntax]
Core.substSubst_form [in syntax]
Core.substSubst_term_pointwise [in syntax]
Core.substSubst_term [in syntax]
Core.substSubst_spec_pointwise [in syntax]
Core.substSubst_spec [in syntax]
Core.substSubst_exp_pointwise [in syntax]
Core.substSubst_exp [in syntax]
Core.substSubst_index_pointwise [in syntax]
Core.substSubst_index [in syntax]
Core.substSubst_prog_pointwise [in syntax]
Core.substSubst_prog [in syntax]
Core.substSubst_type_pointwise [in syntax]
Core.substSubst_type [in syntax]
Core.upExtRen_term_term [in syntax]
Core.upExtRen_exp_exp [in syntax]
Core.upExtRen_exp_prog [in syntax]
Core.upExtRen_exp_type [in syntax]
Core.upExtRen_prog_exp [in syntax]
Core.upExtRen_type_exp [in syntax]
Core.upExtRen_prog_prog [in syntax]
Core.upExtRen_prog_type [in syntax]
Core.upExtRen_type_prog [in syntax]
Core.upExtRen_type_type [in syntax]
Core.upExt_term_term [in syntax]
Core.upExt_exp_exp [in syntax]
Core.upExt_exp_prog [in syntax]
Core.upExt_exp_type [in syntax]
Core.upExt_prog_exp [in syntax]
Core.upExt_type_exp [in syntax]
Core.upExt_prog_prog [in syntax]
Core.upExt_prog_type [in syntax]
Core.upExt_type_prog [in syntax]
Core.upExt_type_type [in syntax]
Core.upId_term_term [in syntax]
Core.upId_exp_exp [in syntax]
Core.upId_exp_prog [in syntax]
Core.upId_exp_type [in syntax]
Core.upId_prog_exp [in syntax]
Core.upId_type_exp [in syntax]
Core.upId_prog_prog [in syntax]
Core.upId_prog_type [in syntax]
Core.upId_type_prog [in syntax]
Core.upId_type_type [in syntax]
Core.upRen_term_term [in syntax]
Core.upRen_exp_exp [in syntax]
Core.upRen_exp_prog [in syntax]
Core.upRen_exp_type [in syntax]
Core.upRen_prog_exp [in syntax]
Core.upRen_type_exp [in syntax]
Core.upRen_prog_prog [in syntax]
Core.upRen_prog_type [in syntax]
Core.upRen_type_prog [in syntax]
Core.upRen_type_type [in syntax]
Core.up_subst_subst_term_term [in syntax]
Core.up_subst_ren_term_term [in syntax]
Core.up_ren_subst_term_term [in syntax]
Core.up_ren_ren_term_term [in syntax]
Core.up_term_term [in syntax]
Core.up_subst_subst_exp_exp [in syntax]
Core.up_subst_subst_exp_prog [in syntax]
Core.up_subst_subst_exp_type [in syntax]
Core.up_subst_subst_prog_exp [in syntax]
Core.up_subst_subst_type_exp [in syntax]
Core.up_subst_ren_exp_exp [in syntax]
Core.up_subst_ren_exp_prog [in syntax]
Core.up_subst_ren_exp_type [in syntax]
Core.up_subst_ren_prog_exp [in syntax]
Core.up_subst_ren_type_exp [in syntax]
Core.up_ren_subst_exp_exp [in syntax]
Core.up_ren_subst_exp_prog [in syntax]
Core.up_ren_subst_exp_type [in syntax]
Core.up_ren_subst_prog_exp [in syntax]
Core.up_ren_subst_type_exp [in syntax]
Core.up_ren_ren_exp_exp [in syntax]
Core.up_ren_ren_exp_prog [in syntax]
Core.up_ren_ren_exp_type [in syntax]
Core.up_ren_ren_prog_exp [in syntax]
Core.up_ren_ren_type_exp [in syntax]
Core.up_exp_exp [in syntax]
Core.up_exp_prog [in syntax]
Core.up_exp_type [in syntax]
Core.up_prog_exp [in syntax]
Core.up_type_exp [in syntax]
Core.up_subst_subst_prog_prog [in syntax]
Core.up_subst_subst_prog_type [in syntax]
Core.up_subst_subst_type_prog [in syntax]
Core.up_subst_ren_prog_prog [in syntax]
Core.up_subst_ren_prog_type [in syntax]
Core.up_subst_ren_type_prog [in syntax]
Core.up_ren_subst_prog_prog [in syntax]
Core.up_ren_subst_prog_type [in syntax]
Core.up_ren_subst_type_prog [in syntax]
Core.up_ren_ren_prog_prog [in syntax]
Core.up_ren_ren_prog_type [in syntax]
Core.up_ren_ren_type_prog [in syntax]
Core.up_prog_prog [in syntax]
Core.up_prog_type [in syntax]
Core.up_type_prog [in syntax]
Core.up_subst_subst_type_type [in syntax]
Core.up_subst_ren_type_type [in syntax]
Core.up_ren_subst_type_type [in syntax]
Core.up_ren_ren_type_type [in syntax]
Core.up_type_type [in syntax]
Core.varLRen'_term_pointwise [in syntax]
Core.varLRen'_term [in syntax]
Core.varLRen'_exp_pointwise [in syntax]
Core.varLRen'_exp [in syntax]
Core.varLRen'_prog_pointwise [in syntax]
Core.varLRen'_prog [in syntax]
Core.varLRen'_type_pointwise [in syntax]
Core.varLRen'_type [in syntax]
Core.varL'_term_pointwise [in syntax]
Core.varL'_term [in syntax]
Core.varL'_exp_pointwise [in syntax]
Core.varL'_exp [in syntax]
Core.varL'_prog_pointwise [in syntax]
Core.varL'_prog [in syntax]
Core.varL'_type_pointwise [in syntax]
Core.varL'_type [in syntax]
D
Diamond_ptred [in EffHOL]F
Fext.instId_form [in syntax]Fext.instId_term [in syntax]
Fext.instId_spec [in syntax]
Fext.instId_exp [in syntax]
Fext.instId_index [in syntax]
Fext.instId_prog [in syntax]
Fext.instId_type [in syntax]
Fext.renRen'_form [in syntax]
Fext.renRen'_term [in syntax]
Fext.renRen'_spec [in syntax]
Fext.renRen'_exp [in syntax]
Fext.renRen'_index [in syntax]
Fext.renRen'_prog [in syntax]
Fext.renRen'_type [in syntax]
Fext.renSubst'_form [in syntax]
Fext.renSubst'_term [in syntax]
Fext.renSubst'_spec [in syntax]
Fext.renSubst'_exp [in syntax]
Fext.renSubst'_index [in syntax]
Fext.renSubst'_prog [in syntax]
Fext.renSubst'_type [in syntax]
Fext.rinstId_form [in syntax]
Fext.rinstId_term [in syntax]
Fext.rinstId_spec [in syntax]
Fext.rinstId_exp [in syntax]
Fext.rinstId_index [in syntax]
Fext.rinstId_prog [in syntax]
Fext.rinstId_type [in syntax]
Fext.rinstInst_form [in syntax]
Fext.rinstInst_term [in syntax]
Fext.rinstInst_spec [in syntax]
Fext.rinstInst_exp [in syntax]
Fext.rinstInst_index [in syntax]
Fext.rinstInst_prog [in syntax]
Fext.rinstInst_type [in syntax]
Fext.substRen'_form [in syntax]
Fext.substRen'_term [in syntax]
Fext.substRen'_spec [in syntax]
Fext.substRen'_exp [in syntax]
Fext.substRen'_index [in syntax]
Fext.substRen'_prog [in syntax]
Fext.substRen'_type [in syntax]
Fext.substSubst'_form [in syntax]
Fext.substSubst'_term [in syntax]
Fext.substSubst'_spec [in syntax]
Fext.substSubst'_exp [in syntax]
Fext.substSubst'_index [in syntax]
Fext.substSubst'_prog [in syntax]
Fext.substSubst'_type [in syntax]
Fext.varLRen_term [in syntax]
Fext.varLRen_exp [in syntax]
Fext.varLRen_prog [in syntax]
Fext.varLRen_type [in syntax]
Fext.varL_term [in syntax]
Fext.varL_exp [in syntax]
Fext.varL_prog [in syntax]
Fext.varL_type [in syntax]
funcomp_assoc [in core]
H
has_sort_unique [in HOL]has_sort_subst' [in HOL]
has_sort_ren' [in HOL]
has_sort_subst [in HOL]
has_sort_ren [in HOL]
has_type_subst' [in EffHOL]
has_type_subst [in EffHOL]
has_kind_subst [in EffHOL]
has_index_ren [in EffHOL]
has_type_ren [in EffHOL]
has_kind_ren [in EffHOL]
has_type_weak [in EffHOL]
has_kind_weak [in EffHOL]
HOL_weak [in HOL]
HOPL_HOL [in EffHOL_to_HOL]
HOPL_ren [in EffHOL]
HOPL_eq [in EffHOL]
HOPL_weak [in EffHOL]
HOPL_Fw [in EffHOL_to_Fw]
ht_tmabs_inv [in EffHOL]
ht_tmabs_inv' [in EffHOL]
ht_tyabs_inv [in EffHOL]
ht_tyabs_inv' [in EffHOL]
ht_ret_inv [in EffHOL]
ht_ret_inv' [in EffHOL]
I
is_prop_subst' [in HOL]is_prop_ren' [in HOL]
is_prop_subst [in HOL]
is_prop_ren [in HOL]
is_spec_ren' [in EffHOL]
is_spec_ren [in EffHOL]
is_index_ren [in EffHOL]
is_value_ren [in EffHOL]
L
lup_app [in EffHOL]lup_map_el [in EffHOL]
M
maxred_ptred [in EffHOL]P
pointwise_forall [in core]ptreds_treds [in EffHOL]
ptred_subst' [in EffHOL]
ptred_subst [in EffHOL]
ptred_ren [in EffHOL]
ptred_refl [in EffHOL]
ptred_treds [in EffHOL]
R
red_has_type [in EffHOL]red_prog_ren [in EffHOL]
S
scons_comp' [in unscoped]scons_eta_id' [in unscoped]
scons_eta' [in unscoped]
scons_comp [in unscoped_axioms]
scons_eta [in unscoped_axioms]
scons_eta_id [in unscoped_axioms]
soundness [in HOL_to_EffHOL]
soundness_Fw [in EffHOL_to_Fw]
soundness_typing_check [in HOL_to_EffHOL]
T
THOL_is_prop [in HOL]THOL_weak [in HOL]
transFw_exp_conv [in EffHOL_to_Fw]
transFw_spec_conv [in EffHOL_to_Fw]
transFw_prog_conv [in EffHOL_to_Fw]
transFw_prog_red [in EffHOL_to_Fw]
transFw_prog_is_value [in EffHOL_to_Fw]
transFw_exp_subst [in EffHOL_to_Fw]
transFw_spec_subst [in EffHOL_to_Fw]
transFw_spec_ren_ctx [in EffHOL_to_Fw]
transFw_exp_ren [in EffHOL_to_Fw]
transFw_spec_ren [in EffHOL_to_Fw]
transFw_prog_subst [in EffHOL_to_Fw]
transFw_prog_ren [in EffHOL_to_Fw]
transFw_exp_has_index [in EffHOL_to_Fw]
transFw_spec_is_spec [in EffHOL_to_Fw]
transFw_index_ren_ctx [in EffHOL_to_Fw]
transFw_index_conv [in EffHOL_to_Fw]
transFw_index_ren [in EffHOL_to_Fw]
transFw_index_subst [in EffHOL_to_Fw]
transFw_index_is_index [in EffHOL_to_Fw]
transFw_prog_has_type [in EffHOL_to_Fw]
transFw_type_conv [in EffHOL_to_Fw]
transFw_type_tred [in EffHOL_to_Fw]
transFw_type_subst [in EffHOL_to_Fw]
transFw_type_ren_ctx [in EffHOL_to_Fw]
transFw_type_ren [in EffHOL_to_Fw]
transFw_type_has_kind [in EffHOL_to_Fw]
trans_term_conv [in EffHOL_to_HOL]
trans_form_conv [in EffHOL_to_HOL]
trans_term_point [in EffHOL_to_HOL]
trans_form_subst' [in EffHOL_to_HOL]
trans_term_subst [in EffHOL_to_HOL]
trans_form_subst [in EffHOL_to_HOL]
trans_form_ren' [in EffHOL_to_HOL]
trans_term_ren' [in EffHOL_to_HOL]
trans_term_ren [in EffHOL_to_HOL]
trans_form_ren [in EffHOL_to_HOL]
trans_term_has_sort [in EffHOL_to_HOL]
trans_form_is_prop [in EffHOL_to_HOL]
trans_sort_conv [in EffHOL_to_HOL]
trans_sort_subst [in EffHOL_to_HOL]
trans_sort_ren [in EffHOL_to_HOL]
trans_SL_up [in HOL_to_EffHOL]
trans_SL_lup [in HOL_to_EffHOL]
trans_SL_lup' [in HOL_to_EffHOL]
trans_is_spec [in HOL_to_EffHOL]
trans_IL_up [in HOL_to_EffHOL]
trans_IL_lup [in HOL_to_EffHOL]
trans_IL_lup' [in HOL_to_EffHOL]
trans_I_inj [in HOL_to_EffHOL]
trans_IL_el [in HOL_to_EffHOL]
trans_IL_length [in HOL_to_EffHOL]
trans_has_kind [in HOL_to_EffHOL]
trans_is_index [in HOL_to_EffHOL]
trans_SL_ren [in HOL_to_EffHOL]
trans_SL_ren' [in HOL_to_EffHOL]
trans_S_subst_spec [in HOL_to_EffHOL]
trans_S_subst' [in HOL_to_EffHOL]
trans_S_subst [in HOL_to_EffHOL]
trans_S_ren [in HOL_to_EffHOL]
trans_T_subst [in HOL_to_EffHOL]
trans_T_ren [in HOL_to_EffHOL]
trans_I_ren [in HOL_to_EffHOL]
trans_I_subst [in HOL_to_EffHOL]
treds_arrow_inv [in EffHOL]
treds_arrow_inv' [in EffHOL]
treds_pi_inv [in EffHOL]
treds_pi_inv' [in EffHOL]
treds_comp_inv [in EffHOL]
treds_comp_inv' [in EffHOL]
treds_conv [in EffHOL]
treds_ptreds [in EffHOL]
treds_comp [in EffHOL]
treds_pi [in EffHOL]
treds_abs [in EffHOL]
treds_arrow2 [in EffHOL]
treds_arrow1 [in EffHOL]
treds_app2 [in EffHOL]
treds_app1 [in EffHOL]
treds_type_trans [in EffHOL]
tred_ptred [in EffHOL]
tred_type_subst [in EffHOL]
tred_type_ren [in EffHOL]
ttrans_has_index [in HOL_to_EffHOL]
ttrans_has_kind [in HOL_to_EffHOL]
ttrans_E_subst_exp [in HOL_to_EffHOL]
ttrans_E_subst [in HOL_to_EffHOL]
ttrans_E_ren [in HOL_to_EffHOL]
ttrans_T_subst [in HOL_to_EffHOL]
ttrans_T_ren [in HOL_to_EffHOL]
U
up_ren_ren [in unscoped]Constructor Index
C
ce_cexp_spec [in EffHOL]ce_cexp_index [in EffHOL]
ce_cexp_type [in EffHOL]
ce_exapp_type [in EffHOL]
ce_exabs [in EffHOL]
ce_beta [in EffHOL]
ce_trans [in EffHOL]
ce_sym [in EffHOL]
ce_refl [in EffHOL]
ci_univ [in EffHOL]
ci_ref_index [in EffHOL]
ci_ref_type [in EffHOL]
ci_refb [in EffHOL]
ci_trans [in EffHOL]
ci_sym [in EffHOL]
ci_refl [in EffHOL]
Core.abs [in syntax]
Core.after [in syntax]
Core.all [in syntax]
Core.app [in syntax]
Core.arrow [in syntax]
Core.bind [in syntax]
Core.cexp [in syntax]
Core.comp [in syntax]
Core.cterm [in syntax]
Core.exabs [in syntax]
Core.exapp [in syntax]
Core.holds [in syntax]
Core.implies [in syntax]
Core.pi [in syntax]
Core.ref [in syntax]
Core.refb [in syntax]
Core.ret [in syntax]
Core.spall [in syntax]
Core.spholds [in syntax]
Core.spimplies [in syntax]
Core.tmabs [in syntax]
Core.tmall [in syntax]
Core.tmapp [in syntax]
Core.tyabs [in syntax]
Core.tyall [in syntax]
Core.tyapp [in syntax]
Core.univ [in syntax]
Core.up_type [in syntax]
Core.up_prog [in syntax]
Core.up_index [in syntax]
Core.up_exp [in syntax]
Core.up_spec [in syntax]
Core.up_term [in syntax]
Core.up_form [in syntax]
Core.var_term [in syntax]
Core.var_exp [in syntax]
Core.var_prog [in syntax]
Core.var_type [in syntax]
cp_tyapp [in EffHOL]
cp_trans [in EffHOL]
cp_sym [in EffHOL]
cp_refl [in EffHOL]
cs_holds_exp2 [in EffHOL]
cs_holds_exp1 [in EffHOL]
cs_holds_prog [in EffHOL]
cs_spall_spec [in EffHOL]
cs_spall_index [in EffHOL]
cs_tmall_spec [in EffHOL]
cs_tmall_type [in EffHOL]
cs_tyall [in EffHOL]
cs_after_spec [in EffHOL]
cs_after_prog [in EffHOL]
cs_implies2 [in EffHOL]
cs_implies1 [in EffHOL]
cs_trans [in EffHOL]
cs_sym [in EffHOL]
cs_refl [in EffHOL]
ct_trans [in EffHOL]
ct_refl [in EffHOL]
ct_tred [in EffHOL]
ct_comp [in EffHOL]
ct_pi [in EffHOL]
ct_arrow2 [in EffHOL]
ct_arrow1 [in EffHOL]
ct_app2 [in EffHOL]
ct_app1 [in EffHOL]
ct_abs [in EffHOL]
ct_beta [in EffHOL]
F
Fw_CONV [in EffHOL_to_Fw]Fw_RED [in EffHOL_to_Fw]
Fw_CE [in EffHOL_to_Fw]
Fw_CI [in EffHOL_to_Fw]
Fw_SAE [in EffHOL_to_Fw]
Fw_SAI [in EffHOL_to_Fw]
Fw_EAE [in EffHOL_to_Fw]
Fw_EAI [in EffHOL_to_Fw]
Fw_TAE [in EffHOL_to_Fw]
Fw_TAI [in EffHOL_to_Fw]
Fw_IE [in EffHOL_to_Fw]
Fw_II [in EffHOL_to_Fw]
Fw_CTX [in EffHOL_to_Fw]
H
hi_conv [in EffHOL]hi_exapp [in EffHOL]
hi_exabs [in EffHOL]
hi_cexp [in EffHOL]
hi_var [in EffHOL]
hi_conv [in EffHOL_to_Fw]
hi_exapp [in EffHOL_to_Fw]
hi_exabs [in EffHOL_to_Fw]
hi_cexp [in EffHOL_to_Fw]
hi_var [in EffHOL_to_Fw]
hk_comp [in EffHOL]
hk_pi [in EffHOL]
hk_arrow [in EffHOL]
hk_abs [in EffHOL]
hk_app [in EffHOL]
hk_var [in EffHOL]
HOL_CE [in HOL]
HOL_CI [in HOL]
HOL_AE [in HOL]
HOL_AI [in HOL]
HOL_IE [in HOL]
HOL_II [in HOL]
HOL_CTX [in HOL]
HOPL_CONV [in EffHOL]
HOPL_RED [in EffHOL]
HOPL_MM [in EffHOL]
HOPL_ME [in EffHOL]
HOPL_MI [in EffHOL]
HOPL_CE [in EffHOL]
HOPL_CI [in EffHOL]
HOPL_SAE [in EffHOL]
HOPL_SAI [in EffHOL]
HOPL_EAE [in EffHOL]
HOPL_EAI [in EffHOL]
HOPL_TAE [in EffHOL]
HOPL_TAI [in EffHOL]
HOPL_IE [in EffHOL]
HOPL_II [in EffHOL]
HOPL_CTX [in EffHOL]
hs_cterm [in HOL]
hs_var [in HOL]
ht_conv [in EffHOL]
ht_tmapp [in EffHOL]
ht_tyapp [in EffHOL]
ht_bind [in EffHOL]
ht_ret [in EffHOL]
ht_tmabs [in EffHOL]
ht_tyabs [in EffHOL]
ht_var [in EffHOL]
ht_conv [in EffHOL_to_Fw]
ht_tmapp [in EffHOL_to_Fw]
ht_tyapp [in EffHOL_to_Fw]
ht_tmabs [in EffHOL_to_Fw]
ht_tyabs [in EffHOL_to_Fw]
ht_var [in EffHOL_to_Fw]
I
ids [in unscoped]ii_univ [in EffHOL]
ii_ref [in EffHOL]
ii_refb [in EffHOL]
ip_holds [in HOL]
ip_all [in HOL]
ip_implies [in HOL]
is_holds [in EffHOL]
is_spall [in EffHOL]
is_tmall [in EffHOL]
is_tyall [in EffHOL]
is_after [in EffHOL]
is_implies [in EffHOL]
is_holds [in EffHOL_to_Fw]
is_spall [in EffHOL_to_Fw]
is_tmall [in EffHOL_to_Fw]
is_tyall [in EffHOL_to_Fw]
is_implies [in EffHOL_to_Fw]
iv_tmabs [in EffHOL]
iv_tyabs [in EffHOL]
iv_var [in EffHOL]
P
pt_trans [in EffHOL]pt_ptred [in EffHOL]
pt_comp [in EffHOL]
pt_pi [in EffHOL]
pt_arrow [in EffHOL]
pt_app [in EffHOL]
pt_abs [in EffHOL]
pt_beta [in EffHOL]
pt_var [in EffHOL]
R
ren1 [in unscoped]ren2 [in unscoped]
ren3 [in unscoped]
ren4 [in unscoped]
ren5 [in unscoped]
rp_ret [in EffHOL]
rp_betatm [in EffHOL]
rp_betaty [in EffHOL]
S
subst1 [in unscoped]subst2 [in unscoped]
subst3 [in unscoped]
subst4 [in unscoped]
subst5 [in unscoped]
T
THOL_CE [in HOL]THOL_CI [in HOL]
THOL_AE [in HOL]
THOL_AI [in HOL]
THOL_IE [in HOL]
THOL_II [in HOL]
THOL_CTX [in HOL]
Inductive Index
C
conv_spec [in EffHOL]conv_exp [in EffHOL]
conv_index [in EffHOL]
conv_prog [in EffHOL]
Core.exp [in syntax]
Core.form [in syntax]
Core.index [in syntax]
Core.prog [in syntax]
Core.spec [in syntax]
Core.term [in syntax]
Core.type [in syntax]
Core.Up_type [in syntax]
Core.Up_prog [in syntax]
Core.Up_index [in syntax]
Core.Up_exp [in syntax]
Core.Up_spec [in syntax]
Core.Up_term [in syntax]
Core.Up_form [in syntax]
F
Fw_prv [in EffHOL_to_Fw]H
has_sort [in HOL]has_index [in EffHOL]
has_type [in EffHOL]
has_kind [in EffHOL]
has_indexFw [in EffHOL_to_Fw]
has_typeFw [in EffHOL_to_Fw]
HOL_prv [in HOL]
HOPL_prv [in EffHOL]
I
is_prop [in HOL]is_spec [in EffHOL]
is_index [in EffHOL]
is_value [in EffHOL]
is_specFw [in EffHOL_to_Fw]
P
ptred [in EffHOL]ptreds [in EffHOL]
R
red_prog [in EffHOL]Ren1 [in unscoped]
Ren2 [in unscoped]
Ren3 [in unscoped]
Ren4 [in unscoped]
Ren5 [in unscoped]
S
Subst1 [in unscoped]Subst2 [in unscoped]
Subst3 [in unscoped]
Subst4 [in unscoped]
Subst5 [in unscoped]
T
THOL_prv [in HOL]treds_type [in EffHOL]
tred_type [in EffHOL]
V
Var [in unscoped]Projection Index
C
Core.up_type [in syntax]Core.up_prog [in syntax]
Core.up_index [in syntax]
Core.up_exp [in syntax]
Core.up_spec [in syntax]
Core.up_term [in syntax]
Core.up_form [in syntax]
I
ids [in unscoped]R
ren1 [in unscoped]ren2 [in unscoped]
ren3 [in unscoped]
ren4 [in unscoped]
ren5 [in unscoped]
S
subst1 [in unscoped]subst2 [in unscoped]
subst3 [in unscoped]
subst4 [in unscoped]
subst5 [in unscoped]
Section Index
F
Fw [in EffHOL_to_Fw]Instance Index
C
Core.ren_type_morphism2 [in syntax]Core.ren_type_morphism [in syntax]
Core.ren_prog_morphism2 [in syntax]
Core.ren_prog_morphism [in syntax]
Core.ren_index_morphism2 [in syntax]
Core.ren_index_morphism [in syntax]
Core.ren_exp_morphism2 [in syntax]
Core.ren_exp_morphism [in syntax]
Core.ren_spec_morphism2 [in syntax]
Core.ren_spec_morphism [in syntax]
Core.ren_term_morphism2 [in syntax]
Core.ren_term_morphism [in syntax]
Core.ren_form_morphism2 [in syntax]
Core.ren_form_morphism [in syntax]
Core.Ren_type [in syntax]
Core.Ren_prog [in syntax]
Core.Ren_index [in syntax]
Core.Ren_exp [in syntax]
Core.Ren_spec [in syntax]
Core.Ren_term [in syntax]
Core.Ren_form [in syntax]
Core.subst_type_morphism2 [in syntax]
Core.subst_type_morphism [in syntax]
Core.subst_prog_morphism2 [in syntax]
Core.subst_prog_morphism [in syntax]
Core.subst_index_morphism2 [in syntax]
Core.subst_index_morphism [in syntax]
Core.subst_exp_morphism2 [in syntax]
Core.subst_exp_morphism [in syntax]
Core.subst_spec_morphism2 [in syntax]
Core.subst_spec_morphism [in syntax]
Core.subst_term_morphism2 [in syntax]
Core.subst_term_morphism [in syntax]
Core.subst_form_morphism2 [in syntax]
Core.subst_form_morphism [in syntax]
Core.Subst_type [in syntax]
Core.Subst_prog [in syntax]
Core.Subst_index [in syntax]
Core.Subst_exp [in syntax]
Core.Subst_spec [in syntax]
Core.Subst_term [in syntax]
Core.Subst_form [in syntax]
Core.Up_type_type [in syntax]
Core.Up_type_prog [in syntax]
Core.Up_prog_type [in syntax]
Core.Up_prog_prog [in syntax]
Core.Up_type_exp [in syntax]
Core.Up_prog_exp [in syntax]
Core.Up_exp_type [in syntax]
Core.Up_exp_prog [in syntax]
Core.Up_exp_exp [in syntax]
Core.Up_term_term [in syntax]
Core.VarInstance_type [in syntax]
Core.VarInstance_prog [in syntax]
Core.VarInstance_exp [in syntax]
Core.VarInstance_term [in syntax]
F
funcomp_morphism2 [in core]funcomp_morphism [in core]
I
idsRen [in unscoped]S
scons_morphism2 [in unscoped]scons_morphism [in unscoped]
Abbreviation Index
L
lup [in HOL]lup [in EffHOL]
lup [in EffHOL_to_Fw]
Definition Index
A
ap [in unscoped]apc [in unscoped]
C
cod [in core_axioms]cod_comp [in core_axioms]
cod_ext [in core_axioms]
cod_id [in core_axioms]
cod_map [in core_axioms]
conv_spec_sind [in EffHOL]
conv_spec_ind [in EffHOL]
conv_exp_sind [in EffHOL]
conv_exp_ind [in EffHOL]
conv_index_sind [in EffHOL]
conv_index_ind [in EffHOL]
conv_prog_sind [in EffHOL]
conv_prog_ind [in EffHOL]
conv_type [in EffHOL]
Core.compRenRen_form [in syntax]
Core.compRenRen_term [in syntax]
Core.compRenRen_spec [in syntax]
Core.compRenRen_exp [in syntax]
Core.compRenRen_index [in syntax]
Core.compRenRen_prog [in syntax]
Core.compRenRen_type [in syntax]
Core.compRenSubst_form [in syntax]
Core.compRenSubst_term [in syntax]
Core.compRenSubst_spec [in syntax]
Core.compRenSubst_exp [in syntax]
Core.compRenSubst_index [in syntax]
Core.compRenSubst_prog [in syntax]
Core.compRenSubst_type [in syntax]
Core.compSubstRen_form [in syntax]
Core.compSubstRen_term [in syntax]
Core.compSubstRen_spec [in syntax]
Core.compSubstRen_exp [in syntax]
Core.compSubstRen_index [in syntax]
Core.compSubstRen_prog [in syntax]
Core.compSubstRen_type [in syntax]
Core.compSubstSubst_form [in syntax]
Core.compSubstSubst_term [in syntax]
Core.compSubstSubst_spec [in syntax]
Core.compSubstSubst_exp [in syntax]
Core.compSubstSubst_index [in syntax]
Core.compSubstSubst_prog [in syntax]
Core.compSubstSubst_type [in syntax]
Core.exp_sind [in syntax]
Core.exp_rec [in syntax]
Core.exp_ind [in syntax]
Core.exp_rect [in syntax]
Core.extRen_form [in syntax]
Core.extRen_term [in syntax]
Core.extRen_spec [in syntax]
Core.extRen_exp [in syntax]
Core.extRen_index [in syntax]
Core.extRen_prog [in syntax]
Core.extRen_type [in syntax]
Core.ext_form [in syntax]
Core.ext_term [in syntax]
Core.ext_spec [in syntax]
Core.ext_exp [in syntax]
Core.ext_index [in syntax]
Core.ext_prog [in syntax]
Core.ext_type [in syntax]
Core.form_sind [in syntax]
Core.form_rec [in syntax]
Core.form_ind [in syntax]
Core.form_rect [in syntax]
Core.idSubst_form [in syntax]
Core.idSubst_term [in syntax]
Core.idSubst_spec [in syntax]
Core.idSubst_exp [in syntax]
Core.idSubst_index [in syntax]
Core.idSubst_prog [in syntax]
Core.idSubst_type [in syntax]
Core.index_sind [in syntax]
Core.index_rec [in syntax]
Core.index_ind [in syntax]
Core.index_rect [in syntax]
Core.prog_sind [in syntax]
Core.prog_rec [in syntax]
Core.prog_ind [in syntax]
Core.prog_rect [in syntax]
Core.ren_form [in syntax]
Core.ren_term [in syntax]
Core.ren_spec [in syntax]
Core.ren_exp [in syntax]
Core.ren_index [in syntax]
Core.ren_prog [in syntax]
Core.ren_type [in syntax]
Core.rinst_inst_form [in syntax]
Core.rinst_inst_term [in syntax]
Core.rinst_inst_spec [in syntax]
Core.rinst_inst_exp [in syntax]
Core.rinst_inst_index [in syntax]
Core.rinst_inst_prog [in syntax]
Core.rinst_inst_type [in syntax]
Core.spec_sind [in syntax]
Core.spec_rec [in syntax]
Core.spec_ind [in syntax]
Core.spec_rect [in syntax]
Core.subst_form [in syntax]
Core.subst_term [in syntax]
Core.subst_spec [in syntax]
Core.subst_exp [in syntax]
Core.subst_index [in syntax]
Core.subst_prog [in syntax]
Core.subst_type [in syntax]
Core.term_sind [in syntax]
Core.term_rec [in syntax]
Core.term_ind [in syntax]
Core.term_rect [in syntax]
Core.type_sind [in syntax]
Core.type_rec [in syntax]
Core.type_ind [in syntax]
Core.type_rect [in syntax]
F
funcomp [in core]Fw_prv_sind [in EffHOL_to_Fw]
Fw_prv_ind [in EffHOL_to_Fw]
H
has_sort_sind [in HOL]has_sort_ind [in HOL]
has_index_sind [in EffHOL]
has_index_ind [in EffHOL]
has_type_sind [in EffHOL]
has_type_ind [in EffHOL]
has_kind_sind [in EffHOL]
has_kind_ind [in EffHOL]
has_indexFw_sind [in EffHOL_to_Fw]
has_indexFw_ind [in EffHOL_to_Fw]
has_typeFw_sind [in EffHOL_to_Fw]
has_typeFw_ind [in EffHOL_to_Fw]
HOL_prv_sind [in HOL]
HOL_prv_ind [in HOL]
HOPL_prv_sind [in EffHOL]
HOPL_prv_ind [in EffHOL]
I
id [in unscoped]is_prop_sind [in HOL]
is_prop_ind [in HOL]
is_spec_sind [in EffHOL]
is_spec_ind [in EffHOL]
is_index_sind [in EffHOL]
is_index_ind [in EffHOL]
is_value_sind [in EffHOL]
is_value_ind [in EffHOL]
is_specFw_sind [in EffHOL_to_Fw]
is_specFw_ind [in EffHOL_to_Fw]
K
kind [in EffHOL]L
list_comp [in core]list_id [in core]
list_ext [in core]
M
maxred [in EffHOL]O
option_comp [in core]option_ext [in core]
option_id [in core]
option_map [in core]
P
prod_comp [in core]prod_ext [in core]
prod_id [in core]
prod_map [in core]
ptreds_sind [in EffHOL]
ptreds_ind [in EffHOL]
ptred_sind [in EffHOL]
ptred_ind [in EffHOL]
R
red_prog_sind [in EffHOL]red_prog_ind [in EffHOL]
S
scons [in unscoped]shift [in unscoped]
sort [in HOL]
swap [in EffHOL]
T
THOL_prv_sind [in HOL]THOL_prv_ind [in HOL]
transFw_exp [in EffHOL_to_Fw]
transFw_spec [in EffHOL_to_Fw]
transFw_index [in EffHOL_to_Fw]
transFw_prog [in EffHOL_to_Fw]
transFw_type [in EffHOL_to_Fw]
trans_term [in EffHOL_to_HOL]
trans_form [in EffHOL_to_HOL]
trans_sort [in EffHOL_to_HOL]
trans_SL' [in EffHOL_to_Fw]
trans_S' [in EffHOL_to_Fw]
trans_T' [in EffHOL_to_Fw]
trans_SL [in HOL_to_EffHOL]
trans_SL' [in HOL_to_EffHOL]
trans_IL [in HOL_to_EffHOL]
trans_IL' [in HOL_to_EffHOL]
trans_S [in HOL_to_EffHOL]
trans_T [in HOL_to_EffHOL]
trans_I [in HOL_to_EffHOL]
treds_type_sind [in EffHOL]
treds_type_ind [in EffHOL]
tred_type_sind [in EffHOL]
tred_type_ind [in EffHOL]
ttrans_E [in HOL_to_EffHOL]
ttrans_T [in HOL_to_EffHOL]
U
up_allfv [in unscoped]up_ren [in unscoped]
V
var_zero [in unscoped]Record Index
C
Core.Up_type [in syntax]Core.Up_prog [in syntax]
Core.Up_index [in syntax]
Core.Up_exp [in syntax]
Core.Up_spec [in syntax]
Core.Up_term [in syntax]
Core.Up_form [in syntax]
R
Ren1 [in unscoped]Ren2 [in unscoped]
Ren3 [in unscoped]
Ren4 [in unscoped]
Ren5 [in unscoped]
S
Subst1 [in unscoped]Subst2 [in unscoped]
Subst3 [in unscoped]
Subst4 [in unscoped]
Subst5 [in unscoped]
V
Var [in 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 | (1116 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 | (71 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 | (8 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 | (19 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 | (10 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 | (460 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 | (202 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 | (49 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 | (18 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 | (1 entry) |
| 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 | (61 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 | (3 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 | (196 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 | (18 entries) |