| 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 | (262 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 | (3 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 | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 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 | (132 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 | (41 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 | (14 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) |
| 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 | (56 entries) |
Global Index
B
Beta [module, in Beta]Beta [library]
Beta.beta_par_trans [definition, in Beta]
Beta.beta_par_shift [lemma, in Beta]
Beta.beta_par_imp_bstar [lemma, in Beta]
Beta.beta_par_refl [lemma, in Beta]
Beta.beta_par_base [constructor, in Beta]
Beta.beta_par_app [constructor, in Beta]
Beta.beta_par_lam [constructor, in Beta]
Beta.beta_par_var [constructor, in Beta]
Beta.beta_par [inductive, in Beta]
Beta.bred [inductive, in Beta]
Beta.bred_imp_beta_par [lemma, in Beta]
Beta.bred_halt [definition, in Beta]
Beta.bred_lift_closed [lemma, in Beta]
Beta.bred_appr [constructor, in Beta]
Beta.bred_appl [constructor, in Beta]
Beta.bred_lam [constructor, in Beta]
Beta.bred_base [constructor, in Beta]
Beta.bstar [definition, in Beta]
Beta.bstar_eq_closure_of_beta_par [lemma, in Beta]
Beta.bstar_subst_closed [lemma, in Beta]
Beta.bstar_weak_subst [lemma, in Beta]
Beta.bstar_lift_closed [lemma, in Beta]
Beta.bstar_bred_closed [lemma, in Beta]
Beta.bstar_app_closed [lemma, in Beta]
Beta.bstar_app_closed_r [lemma, in Beta]
Beta.bstar_app_closed_l [lemma, in Beta]
Beta.bstar_lam_closed [lemma, in Beta]
Beta.bstar_reflexive [lemma, in Beta]
Beta.bstar_trans [definition, in Beta]
Beta.bstar_refl [definition, in Beta]
Beta.bstar_step [definition, in Beta]
Beta.inner_bred [definition, in Beta]
Beta.triv_bred [definition, in Beta]
D
DeBruijn [module, in Untyped]DeBruijn.App [constructor, in Untyped]
DeBruijn.Lam [constructor, in Untyped]
DeBruijn.lterm [inductive, in Untyped]
DeBruijn.Var [constructor, in Untyped]
dename [definition, in Untyped]
dename' [definition, in Untyped]
E
Eta [module, in Eta]Eta [library]
Eta.eta [definition, in Eta]
Eta.eta_par_lam_k_lam [lemma, in Eta]
Eta.eta_par_lam_k_app [lemma, in Eta]
Eta.eta_par_lam_k_var [lemma, in Eta]
Eta.eta_star_eq_closure_of_eta_par [lemma, in Eta]
Eta.eta_par_trans [definition, in Eta]
Eta.eta_par_imp_eta_star [lemma, in Eta]
Eta.eta_imp_eta_par [lemma, in Eta]
Eta.eta_par_subst_closed [lemma, in Eta]
Eta.eta_par_substitutive [lemma, in Eta]
Eta.eta_par_lift_closed [lemma, in Eta]
Eta.eta_par_refl [lemma, in Eta]
Eta.eta_par_base [constructor, in Eta]
Eta.eta_par_app [constructor, in Eta]
Eta.eta_par_lam [constructor, in Eta]
Eta.eta_par_var [constructor, in Eta]
Eta.eta_par [inductive, in Eta]
Eta.eta_star_base_closed [lemma, in Eta]
Eta.eta_star_lift_closed [lemma, in Eta]
Eta.eta_star_app_closed [lemma, in Eta]
Eta.eta_star_app_closed_r [lemma, in Eta]
Eta.eta_star_app_closed_l [lemma, in Eta]
Eta.eta_star_lam_closed [lemma, in Eta]
Eta.eta_star_trans [definition, in Eta]
Eta.eta_star_refl [definition, in Eta]
Eta.eta_star_step [definition, in Eta]
Eta.eta_star [definition, in Eta]
Eta.eta_lift_closed [lemma, in Eta]
Eta.eta_prim_lift_closed [lemma, in Eta]
Eta.eta_substitutive [lemma, in Eta]
Eta.eta_prim_substitutive [lemma, in Eta]
Eta.eta_base [constructor, in Eta]
Eta.eta_prim [inductive, in Eta]
Eta.ex1_eta [definition, in Eta]
Eta.ex2_eta [definition, in Eta]
Eta.ex3_eta [definition, in Eta]
Eta.lam_k_eta_red [lemma, in Eta]
Eta.lam_k_zero [definition, in Eta]
Eta.lam_k_alt [lemma, in Eta]
Eta.lam_k [definition, in Eta]
Eta.shift_0_lam_commute [lemma, in Eta]
H
hide [definition, in Untyped]K
k_comb_impl [definition, in Untyped]k_comb [definition, in Untyped]
L
lift [definition, in Subst]lift_lam [lemma, in Subst]
lift_app [lemma, in Subst]
lift_distr_subst [lemma, in Subst]
lift_lift_rev [lemma, in Subst]
lift_lift [lemma, in Subst]
lift_lem3 [lemma, in Subst]
lift_lem2 [lemma, in Subst]
lift_fuse [lemma, in Subst]
lift_0_ident [lemma, in Subst]
lookup [definition, in Untyped]
P
Postpone [module, in Postpone]Postpone [library]
Postpone.beta_eta_star [definition, in Postpone]
Postpone.beta_eta [definition, in Postpone]
Postpone.beta_par_lam_k_closed [lemma, in Postpone]
Postpone.eta_postponement [lemma, in Postpone]
Postpone.eta_postponement_basic [lemma, in Postpone]
Postpone.eta_baby_postpone_beta [lemma, in Postpone]
Postpone.eta_baby_postpone_eta [lemma, in Postpone]
Postpone.lam_S_k_beta [lemma, in Postpone]
Postpone.lam_k_beta_app [lemma, in Postpone]
Postpone.lam_k_beta_lam [lemma, in Postpone]
Postpone.lam_k_beta_subst [lemma, in Postpone]
Postpone.par_impl_par_trans [lemma, in Postpone]
Postpone.postpone_par [lemma, in Postpone]
Postpone.rewrite_existential_beta [lemma, in Postpone]
Postpone.rewrite_existential_eta [lemma, in Postpone]
Postpone.star_exists_iff_par_exists [lemma, in Postpone]
prettier [definition, in Untyped]
PrettyTerm [module, in Untyped]
PrettyTerm.App [constructor, in Untyped]
PrettyTerm.Lam [constructor, in Untyped]
PrettyTerm.pterm [inductive, in Untyped]
PrettyTerm.Var [constructor, in Untyped]
R
Rels [module, in Rels]Rels [library]
Rels.clos_appr [constructor, in Rels]
Rels.clos_appl [constructor, in Rels]
Rels.clos_lam [constructor, in Rels]
Rels.clos_base [constructor, in Rels]
Rels.clos_compat [inductive, in Rels]
Rels.CompatClosure [section, in Rels]
Rels.CompatClosure.rel [variable, in Rels]
S
shift [definition, in Subst]Standardization [module, in Standardization]
Standardization [library]
Standardization.appl [definition, in Standardization]
Standardization.appr [definition, in Standardization]
Standardization.appr_cons [lemma, in Standardization]
Standardization.bet [definition, in Standardization]
Standardization.betstar [definition, in Standardization]
Standardization.betstar_stseq [lemma, in Standardization]
Standardization.betstar_st [lemma, in Standardization]
Standardization.betstar_trans [definition, in Standardization]
Standardization.betstar_refl [definition, in Standardization]
Standardization.betstar_step [definition, in Standardization]
Standardization.bet_bred [lemma, in Standardization]
Standardization.hap [inductive, in Standardization]
Standardization.hap__hap_subst [lemma, in Standardization]
Standardization.hap_st__st [lemma, in Standardization]
Standardization.hap__app_hap [lemma, in Standardization]
Standardization.hap_lstar [lemma, in Standardization]
Standardization.hap_trans [constructor, in Standardization]
Standardization.hap_hred [constructor, in Standardization]
Standardization.hap_refl [constructor, in Standardization]
Standardization.hap' [inductive, in Standardization]
Standardization.hap'_hreds [constructor, in Standardization]
Standardization.hap'_hred [constructor, in Standardization]
Standardization.ladjust [definition, in Standardization]
Standardization.lambdize [definition, in Standardization]
Standardization.leftexpand [definition, in Standardization]
Standardization.leftexpand_monotone [lemma, in Standardization]
Standardization.leftexpand_bound [lemma, in Standardization]
Standardization.leftexpand_seqlast [lemma, in Standardization]
Standardization.leftexpand_seqhead [lemma, in Standardization]
Standardization.lift_st [lemma, in Standardization]
Standardization.lift_first_hap [lemma, in Standardization]
Standardization.lift_hap [lemma, in Standardization]
Standardization.lift_hap' [lemma, in Standardization]
Standardization.lmost [definition, in Standardization]
Standardization.lstar [definition, in Standardization]
Standardization.lstar_trans [definition, in Standardization]
Standardization.lstar_refl [definition, in Standardization]
Standardization.lstar_step [definition, in Standardization]
Standardization.monotone [inductive, in Standardization]
Standardization.monotone_zip [lemma, in Standardization]
Standardization.monotone_connectives [lemma, in Standardization]
Standardization.monotone_seqcat [lemma, in Standardization]
Standardization.monotone_appr [lemma, in Standardization]
Standardization.monotone_appl [lemma, in Standardization]
Standardization.monotone_seqn [lemma, in Standardization]
Standardization.monotone_cons [constructor, in Standardization]
Standardization.monotone_unit [constructor, in Standardization]
Standardization.nthred [inductive, in Standardization]
Standardization.nthred_redcount [lemma, in Standardization]
Standardization.nthred_radjust [lemma, in Standardization]
Standardization.nthred_outer_lam [lemma, in Standardization]
Standardization.nthred_lam [constructor, in Standardization]
Standardization.nthred_concl [constructor, in Standardization]
Standardization.nthred_concr [constructor, in Standardization]
Standardization.nthred_base [constructor, in Standardization]
Standardization.radjust [definition, in Standardization]
Standardization.redcount [definition, in Standardization]
Standardization.redcount_seqn [lemma, in Standardization]
Standardization.redseq [inductive, in Standardization]
Standardization.redseq_zip [lemma, in Standardization]
Standardization.redseq_appr [lemma, in Standardization]
Standardization.redseq_appl [lemma, in Standardization]
Standardization.redseq_seqcat [lemma, in Standardization]
Standardization.redseq_cons [constructor, in Standardization]
Standardization.redseq_unit [constructor, in Standardization]
Standardization.seq [inductive, in Standardization]
Standardization.seqcat [definition, in Standardization]
Standardization.seqcat_leftexpand [lemma, in Standardization]
Standardization.seqhead [definition, in Standardization]
Standardization.seqhead_lambdize [lemma, in Standardization]
Standardization.seqhead_appr [lemma, in Standardization]
Standardization.seqhead_appl [lemma, in Standardization]
Standardization.seqlast [definition, in Standardization]
Standardization.seqlast_lambdize [lemma, in Standardization]
Standardization.seqlast_appr [lemma, in Standardization]
Standardization.seqlast_appl [lemma, in Standardization]
Standardization.seqlast_seqcat [lemma, in Standardization]
Standardization.seqn [definition, in Standardization]
Standardization.seqnrev [definition, in Standardization]
Standardization.seqn_lambdize [lemma, in Standardization]
Standardization.seqn_appl_app [lemma, in Standardization]
Standardization.seqn_appl_lam [lemma, in Standardization]
Standardization.seqn_appl_var [lemma, in Standardization]
Standardization.seqn_seqcat [lemma, in Standardization]
Standardization.seq_cons [constructor, in Standardization]
Standardization.seq_unit [constructor, in Standardization]
Standardization.st [inductive, in Standardization]
Standardization.stseq [definition, in Standardization]
Standardization.stseq_lambda [lemma, in Standardization]
Standardization.stseq_lambdize [lemma, in Standardization]
Standardization.stseq_appr [lemma, in Standardization]
Standardization.stseq_appl [lemma, in Standardization]
Standardization.stseq_unit [lemma, in Standardization]
Standardization.stseq_leftexpand [lemma, in Standardization]
Standardization.stseq_backwards [lemma, in Standardization]
Standardization.st_bred__st [lemma, in Standardization]
Standardization.st_nthred__st [lemma, in Standardization]
Standardization.st_app__st_subst [lemma, in Standardization]
Standardization.st_st__st_subst [lemma, in Standardization]
Standardization.st_refl [lemma, in Standardization]
Standardization.st_stseq [lemma, in Standardization]
Standardization.st_haplam_st [constructor, in Standardization]
Standardization.st_hap_st_st [constructor, in Standardization]
Standardization.st_hap [constructor, in Standardization]
Standardization.subst_indist [lemma, in Standardization]
Standardization.subst_to_var [lemma, in Standardization]
Standardization.subst_hap' [lemma, in Standardization]
Standardization.zip [definition, in Standardization]
Standardization.zip_stseq [lemma, in Standardization]
Standardization.zip_seqlast [lemma, in Standardization]
Standardization.zip_seqhead [lemma, in Standardization]
Standardization.zip_seqhead_right [lemma, in Standardization]
Standardization.zip_appl [lemma, in Standardization]
Standardization.zip_appr [lemma, in Standardization]
subst [definition, in Subst]
Subst [library]
subst_lam [lemma, in Subst]
subst_app [lemma, in Subst]
subst_k_shift_S_k [lemma, in Subst]
subst_shift_ident [lemma, in Subst]
subst_lemma [lemma, in Subst]
s_comb [definition, in Untyped]
U
Untyped [library]V
var_subst_lemma [lemma, in Subst]other
_ $ _ [notation, in Untyped]\ _ ~> _ [notation, in Untyped]
` _ [notation, in Untyped]
Notation Index
other
_ $ _ [in Untyped]\ _ ~> _ [in Untyped]
` _ [in Untyped]
Module Index
B
Beta [in Beta]D
DeBruijn [in Untyped]E
Eta [in Eta]P
Postpone [in Postpone]PrettyTerm [in Untyped]
R
Rels [in Rels]S
Standardization [in Standardization]Variable Index
R
Rels.CompatClosure.rel [in Rels]Library Index
B
BetaE
EtaP
PostponeR
RelsS
StandardizationSubst
U
UntypedLemma Index
B
Beta.beta_par_shift [in Beta]Beta.beta_par_imp_bstar [in Beta]
Beta.beta_par_refl [in Beta]
Beta.bred_imp_beta_par [in Beta]
Beta.bred_lift_closed [in Beta]
Beta.bstar_eq_closure_of_beta_par [in Beta]
Beta.bstar_subst_closed [in Beta]
Beta.bstar_weak_subst [in Beta]
Beta.bstar_lift_closed [in Beta]
Beta.bstar_bred_closed [in Beta]
Beta.bstar_app_closed [in Beta]
Beta.bstar_app_closed_r [in Beta]
Beta.bstar_app_closed_l [in Beta]
Beta.bstar_lam_closed [in Beta]
Beta.bstar_reflexive [in Beta]
E
Eta.eta_par_lam_k_lam [in Eta]Eta.eta_par_lam_k_app [in Eta]
Eta.eta_par_lam_k_var [in Eta]
Eta.eta_star_eq_closure_of_eta_par [in Eta]
Eta.eta_par_imp_eta_star [in Eta]
Eta.eta_imp_eta_par [in Eta]
Eta.eta_par_subst_closed [in Eta]
Eta.eta_par_substitutive [in Eta]
Eta.eta_par_lift_closed [in Eta]
Eta.eta_par_refl [in Eta]
Eta.eta_star_base_closed [in Eta]
Eta.eta_star_lift_closed [in Eta]
Eta.eta_star_app_closed [in Eta]
Eta.eta_star_app_closed_r [in Eta]
Eta.eta_star_app_closed_l [in Eta]
Eta.eta_star_lam_closed [in Eta]
Eta.eta_lift_closed [in Eta]
Eta.eta_prim_lift_closed [in Eta]
Eta.eta_substitutive [in Eta]
Eta.eta_prim_substitutive [in Eta]
Eta.lam_k_eta_red [in Eta]
Eta.lam_k_alt [in Eta]
Eta.shift_0_lam_commute [in Eta]
L
lift_lam [in Subst]lift_app [in Subst]
lift_distr_subst [in Subst]
lift_lift_rev [in Subst]
lift_lift [in Subst]
lift_lem3 [in Subst]
lift_lem2 [in Subst]
lift_fuse [in Subst]
lift_0_ident [in Subst]
P
Postpone.beta_par_lam_k_closed [in Postpone]Postpone.eta_postponement [in Postpone]
Postpone.eta_postponement_basic [in Postpone]
Postpone.eta_baby_postpone_beta [in Postpone]
Postpone.eta_baby_postpone_eta [in Postpone]
Postpone.lam_S_k_beta [in Postpone]
Postpone.lam_k_beta_app [in Postpone]
Postpone.lam_k_beta_lam [in Postpone]
Postpone.lam_k_beta_subst [in Postpone]
Postpone.par_impl_par_trans [in Postpone]
Postpone.postpone_par [in Postpone]
Postpone.rewrite_existential_beta [in Postpone]
Postpone.rewrite_existential_eta [in Postpone]
Postpone.star_exists_iff_par_exists [in Postpone]
S
Standardization.appr_cons [in Standardization]Standardization.betstar_stseq [in Standardization]
Standardization.betstar_st [in Standardization]
Standardization.bet_bred [in Standardization]
Standardization.hap__hap_subst [in Standardization]
Standardization.hap_st__st [in Standardization]
Standardization.hap__app_hap [in Standardization]
Standardization.hap_lstar [in Standardization]
Standardization.leftexpand_monotone [in Standardization]
Standardization.leftexpand_bound [in Standardization]
Standardization.leftexpand_seqlast [in Standardization]
Standardization.leftexpand_seqhead [in Standardization]
Standardization.lift_st [in Standardization]
Standardization.lift_first_hap [in Standardization]
Standardization.lift_hap [in Standardization]
Standardization.lift_hap' [in Standardization]
Standardization.monotone_zip [in Standardization]
Standardization.monotone_connectives [in Standardization]
Standardization.monotone_seqcat [in Standardization]
Standardization.monotone_appr [in Standardization]
Standardization.monotone_appl [in Standardization]
Standardization.monotone_seqn [in Standardization]
Standardization.nthred_redcount [in Standardization]
Standardization.nthred_radjust [in Standardization]
Standardization.nthred_outer_lam [in Standardization]
Standardization.redcount_seqn [in Standardization]
Standardization.redseq_zip [in Standardization]
Standardization.redseq_appr [in Standardization]
Standardization.redseq_appl [in Standardization]
Standardization.redseq_seqcat [in Standardization]
Standardization.seqcat_leftexpand [in Standardization]
Standardization.seqhead_lambdize [in Standardization]
Standardization.seqhead_appr [in Standardization]
Standardization.seqhead_appl [in Standardization]
Standardization.seqlast_lambdize [in Standardization]
Standardization.seqlast_appr [in Standardization]
Standardization.seqlast_appl [in Standardization]
Standardization.seqlast_seqcat [in Standardization]
Standardization.seqn_lambdize [in Standardization]
Standardization.seqn_appl_app [in Standardization]
Standardization.seqn_appl_lam [in Standardization]
Standardization.seqn_appl_var [in Standardization]
Standardization.seqn_seqcat [in Standardization]
Standardization.stseq_lambda [in Standardization]
Standardization.stseq_lambdize [in Standardization]
Standardization.stseq_appr [in Standardization]
Standardization.stseq_appl [in Standardization]
Standardization.stseq_unit [in Standardization]
Standardization.stseq_leftexpand [in Standardization]
Standardization.stseq_backwards [in Standardization]
Standardization.st_bred__st [in Standardization]
Standardization.st_nthred__st [in Standardization]
Standardization.st_app__st_subst [in Standardization]
Standardization.st_st__st_subst [in Standardization]
Standardization.st_refl [in Standardization]
Standardization.st_stseq [in Standardization]
Standardization.subst_indist [in Standardization]
Standardization.subst_to_var [in Standardization]
Standardization.subst_hap' [in Standardization]
Standardization.zip_stseq [in Standardization]
Standardization.zip_seqlast [in Standardization]
Standardization.zip_seqhead [in Standardization]
Standardization.zip_seqhead_right [in Standardization]
Standardization.zip_appl [in Standardization]
Standardization.zip_appr [in Standardization]
subst_lam [in Subst]
subst_app [in Subst]
subst_k_shift_S_k [in Subst]
subst_shift_ident [in Subst]
subst_lemma [in Subst]
V
var_subst_lemma [in Subst]Constructor Index
B
Beta.beta_par_base [in Beta]Beta.beta_par_app [in Beta]
Beta.beta_par_lam [in Beta]
Beta.beta_par_var [in Beta]
Beta.bred_appr [in Beta]
Beta.bred_appl [in Beta]
Beta.bred_lam [in Beta]
Beta.bred_base [in Beta]
D
DeBruijn.App [in Untyped]DeBruijn.Lam [in Untyped]
DeBruijn.Var [in Untyped]
E
Eta.eta_par_base [in Eta]Eta.eta_par_app [in Eta]
Eta.eta_par_lam [in Eta]
Eta.eta_par_var [in Eta]
Eta.eta_base [in Eta]
P
PrettyTerm.App [in Untyped]PrettyTerm.Lam [in Untyped]
PrettyTerm.Var [in Untyped]
R
Rels.clos_appr [in Rels]Rels.clos_appl [in Rels]
Rels.clos_lam [in Rels]
Rels.clos_base [in Rels]
S
Standardization.hap_trans [in Standardization]Standardization.hap_hred [in Standardization]
Standardization.hap_refl [in Standardization]
Standardization.hap'_hreds [in Standardization]
Standardization.hap'_hred [in Standardization]
Standardization.monotone_cons [in Standardization]
Standardization.monotone_unit [in Standardization]
Standardization.nthred_lam [in Standardization]
Standardization.nthred_concl [in Standardization]
Standardization.nthred_concr [in Standardization]
Standardization.nthred_base [in Standardization]
Standardization.redseq_cons [in Standardization]
Standardization.redseq_unit [in Standardization]
Standardization.seq_cons [in Standardization]
Standardization.seq_unit [in Standardization]
Standardization.st_haplam_st [in Standardization]
Standardization.st_hap_st_st [in Standardization]
Standardization.st_hap [in Standardization]
Inductive Index
B
Beta.beta_par [in Beta]Beta.bred [in Beta]
D
DeBruijn.lterm [in Untyped]E
Eta.eta_par [in Eta]Eta.eta_prim [in Eta]
P
PrettyTerm.pterm [in Untyped]R
Rels.clos_compat [in Rels]S
Standardization.hap [in Standardization]Standardization.hap' [in Standardization]
Standardization.monotone [in Standardization]
Standardization.nthred [in Standardization]
Standardization.redseq [in Standardization]
Standardization.seq [in Standardization]
Standardization.st [in Standardization]
Section Index
R
Rels.CompatClosure [in Rels]Definition Index
B
Beta.beta_par_trans [in Beta]Beta.bred_halt [in Beta]
Beta.bstar [in Beta]
Beta.bstar_trans [in Beta]
Beta.bstar_refl [in Beta]
Beta.bstar_step [in Beta]
Beta.inner_bred [in Beta]
Beta.triv_bred [in Beta]
D
dename [in Untyped]dename' [in Untyped]
E
Eta.eta [in Eta]Eta.eta_par_trans [in Eta]
Eta.eta_star_trans [in Eta]
Eta.eta_star_refl [in Eta]
Eta.eta_star_step [in Eta]
Eta.eta_star [in Eta]
Eta.ex1_eta [in Eta]
Eta.ex2_eta [in Eta]
Eta.ex3_eta [in Eta]
Eta.lam_k_zero [in Eta]
Eta.lam_k [in Eta]
H
hide [in Untyped]K
k_comb_impl [in Untyped]k_comb [in Untyped]
L
lift [in Subst]lookup [in Untyped]
P
Postpone.beta_eta_star [in Postpone]Postpone.beta_eta [in Postpone]
prettier [in Untyped]
S
shift [in Subst]Standardization.appl [in Standardization]
Standardization.appr [in Standardization]
Standardization.bet [in Standardization]
Standardization.betstar [in Standardization]
Standardization.betstar_trans [in Standardization]
Standardization.betstar_refl [in Standardization]
Standardization.betstar_step [in Standardization]
Standardization.ladjust [in Standardization]
Standardization.lambdize [in Standardization]
Standardization.leftexpand [in Standardization]
Standardization.lmost [in Standardization]
Standardization.lstar [in Standardization]
Standardization.lstar_trans [in Standardization]
Standardization.lstar_refl [in Standardization]
Standardization.lstar_step [in Standardization]
Standardization.radjust [in Standardization]
Standardization.redcount [in Standardization]
Standardization.seqcat [in Standardization]
Standardization.seqhead [in Standardization]
Standardization.seqlast [in Standardization]
Standardization.seqn [in Standardization]
Standardization.seqnrev [in Standardization]
Standardization.stseq [in Standardization]
Standardization.zip [in Standardization]
subst [in Subst]
s_comb [in Untyped]
| 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 | (262 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 | (3 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 | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 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 | (132 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 | (41 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 | (14 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) |
| 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 | (56 entries) |
This page has been generated by coqdoc