| 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 | (1624 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 | (78 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 | (2 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 | (77 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 | (30 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 | (524 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 | (348 entries) |
| Axiom 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) |
| 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 | (60 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 | (26 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (123 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 | (18 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 | (9 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (315 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 | (13 entries) |
Global Index
A
AbstractReductionSystems [library]active [definition, in CBPV.StrongNormalisation]
activev [definition, in CBPV.StrongNormalisation]
adequacy [lemma, in CBPV.DenotationalSemantics]
Adequacy [lemma, in CBPV.CBN.DenotationalSemantics]
Adequacy [lemma, in CBPV.CBV.DenotationalSemantics]
adequacyᵥ [lemma, in CBPV.DenotationalSemantics]
Adequacyᵥ [lemma, in CBPV.CBV.DenotationalSemantics]
algstruct [projection, in CBPV.DenotationalSemantics]
ap [definition, in CBPV.fintype]
apc [definition, in CBPV.fintype]
app [constructor, in CBPV.Syntax]
App [constructor, in CBPV.CBN.CBN]
App [constructor, in CBPV.CBV.CBV]
Arr [constructor, in CBPV.CBN.CBN]
Arr [constructor, in CBPV.CBV.CBV]
arrow [constructor, in CBPV.Syntax]
arrow [constructor, in CBPV.Terms]
axioms [library]
B
backwards [lemma, in CBPV.CBN.weakStory]backwards_evaluates [lemma, in CBPV.CBN.weakStory]
backwards_termination [lemma, in CBPV.CBV.strongStory]
backwards_termination [lemma, in CBPV.CBV.weakStory]
backwards_steps [lemma, in CBPV.CBV.weakStory]
backwards_step [lemma, in CBPV.CBV.weakStory]
backward_simulation [lemma, in CBPV.CBV.weakStory]
Base [library]
basic_lemma [lemma, in CBPV.DenotationalSemantics]
beta_step_preserved [lemma, in CBPV.CBN.strongStory]
beta_lift [lemma, in CBPV.Confluence]
beta₂_lift [lemma, in CBPV.Confluence]
bigstep [inductive, in CBPV.Semantics]
bigstepApp [constructor, in CBPV.Semantics]
bigstepCaseP [constructor, in CBPV.Semantics]
bigstepCaseS [constructor, in CBPV.Semantics]
bigstepCu [constructor, in CBPV.Semantics]
bigstepForce [constructor, in CBPV.Semantics]
bigstepLambda [constructor, in CBPV.Semantics]
bigstepLetin [constructor, in CBPV.Semantics]
bigstepProj [constructor, in CBPV.Semantics]
bigstepReturn [constructor, in CBPV.Semantics]
bigstepTuple [constructor, in CBPV.Semantics]
bigstep_sn [lemma, in CBPV.Semantics]
bigstep_sn' [lemma, in CBPV.Semantics]
bigstep_normal [lemma, in CBPV.Semantics]
bigstep_functional [lemma, in CBPV.Semantics]
bigstep_prepend [lemma, in CBPV.Semantics]
bigstep_cons [lemma, in CBPV.Semantics]
bigstep_primitive_cons [lemma, in CBPV.Semantics]
bigstep_soundness [lemma, in CBPV.Semantics]
bind [lemma, in CBPV.LogicalEquivalence]
Bool [definition, in CBPV.CBN.DenotationalSemantics]
Bool [definition, in CBPV.CBV.DenotationalSemantics]
bound [definition, in CBPV.fintype]
C
C [definition, in CBPV.LogicalEquivalence]C [definition, in CBPV.SemanticTyping]
C [definition, in CBPV.StrongNormalisation]
Carrier [projection, in CBPV.DenotationalSemantics]
caseP [constructor, in CBPV.Syntax]
CaseP [constructor, in CBPV.CBV.CBV]
caseS [constructor, in CBPV.Syntax]
CaseS [constructor, in CBPV.CBN.CBN]
CaseS [constructor, in CBPV.CBV.CBV]
caseScott [definition, in CBPV.CBN.DenotationalSemantics]
caseZ [constructor, in CBPV.Syntax]
CBN [record, in CBPV.CBN.DenotationalSemantics]
CBN [library]
CBN_H [projection, in CBPV.CBN.DenotationalSemantics]
CBN_e [projection, in CBPV.CBN.DenotationalSemantics]
cbn_type_pres' [lemma, in CBPV.CBN.DenotationalSemantics]
cbn_type_pres [lemma, in CBPV.CBN.CBN_CBPV]
cbn_typepres_substitution [definition, in CBPV.CBN.CBN_CBPV]
cbn_typepres_renaming [definition, in CBPV.CBN.CBN_CBPV]
cbn_typeVar' [lemma, in CBPV.CBN.CBN_CBPV]
cbn_typeApp [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typeCaseS [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typeInj [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typeProj [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typePair [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typeLam [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typeUnit [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typeVar [constructor, in CBPV.CBN.CBN_CBPV]
cbn_typing [inductive, in CBPV.CBN.CBN_CBPV]
cbn_ctx [definition, in CBPV.CBN.CBN_CBPV]
CBN_CBPV [library]
CBPVc [record, in CBPV.ObservationalEquivalence]
CBPVc_H [projection, in CBPV.ObservationalEquivalence]
CBPVc_c [projection, in CBPV.ObservationalEquivalence]
CBPVv [record, in CBPV.ObservationalEquivalence]
CBPVv_H [projection, in CBPV.ObservationalEquivalence]
CBPVv_v [projection, in CBPV.ObservationalEquivalence]
CBV [record, in CBPV.CBV.DenotationalSemantics]
CBV [library]
CBV_Hᵥ [projection, in CBPV.CBV.DenotationalSemantics]
CBV_v [projection, in CBPV.CBV.DenotationalSemantics]
CBV_H [projection, in CBPV.CBV.DenotationalSemantics]
CBV_e [projection, in CBPV.CBV.DenotationalSemantics]
CBV_CBPV [library]
CBVᵥ [record, in CBPV.CBV.DenotationalSemantics]
CCBPVc [definition, in CBPV.DenotationalSemantics]
CCBPVv [definition, in CBPV.DenotationalSemantics]
cctx [inductive, in CBPV.ProgramContexts]
cctxAppL [constructor, in CBPV.ProgramContexts]
cctxAppR [constructor, in CBPV.ProgramContexts]
cctxCasePC [constructor, in CBPV.ProgramContexts]
cctxCasePV [constructor, in CBPV.ProgramContexts]
cctxCaseSL [constructor, in CBPV.ProgramContexts]
cctxCaseSR [constructor, in CBPV.ProgramContexts]
cctxCaseSV [constructor, in CBPV.ProgramContexts]
cctxCaseZ [constructor, in CBPV.ProgramContexts]
cctxForce [constructor, in CBPV.ProgramContexts]
cctxHole [constructor, in CBPV.ProgramContexts]
cctxLambda [constructor, in CBPV.ProgramContexts]
cctxLetinL [constructor, in CBPV.ProgramContexts]
cctxLetinR [constructor, in CBPV.ProgramContexts]
cctxProj [constructor, in CBPV.ProgramContexts]
cctxRet [constructor, in CBPV.ProgramContexts]
cctxTupleL [constructor, in CBPV.ProgramContexts]
cctxTupleR [constructor, in CBPV.ProgramContexts]
cctxTyping [inductive, in CBPV.ProgramContexts]
cctxTypingAppL [constructor, in CBPV.ProgramContexts]
cctxTypingAppR [constructor, in CBPV.ProgramContexts]
cctxTypingCasePC [constructor, in CBPV.ProgramContexts]
cctxTypingCasePV [constructor, in CBPV.ProgramContexts]
cctxTypingCaseSL [constructor, in CBPV.ProgramContexts]
cctxTypingCaseSR [constructor, in CBPV.ProgramContexts]
cctxTypingCaseSV [constructor, in CBPV.ProgramContexts]
cctxTypingCaseZ [constructor, in CBPV.ProgramContexts]
cctxTypingForce [constructor, in CBPV.ProgramContexts]
cctxTypingHole [constructor, in CBPV.ProgramContexts]
cctxTypingLambda [constructor, in CBPV.ProgramContexts]
cctxTypingLetinL [constructor, in CBPV.ProgramContexts]
cctxTypingLetinR [constructor, in CBPV.ProgramContexts]
cctxTypingProj [constructor, in CBPV.ProgramContexts]
cctxTypingRet [constructor, in CBPV.ProgramContexts]
cctxTypingTupleL [constructor, in CBPV.ProgramContexts]
cctxTypingTupleR [constructor, in CBPV.ProgramContexts]
cctx_comp_typing_soundness [definition, in CBPV.ProgramContexts]
cctx_value_typing_soundness [definition, in CBPV.ProgramContexts]
cctx_cctx_plug_typing_soundness [definition, in CBPV.ProgramContexts]
cctx_vctx_plug_typing_soundness [definition, in CBPV.ProgramContexts]
cctx_typing_ind_3 [definition, in CBPV.ProgramContexts]
cctx_typing_ind_2 [definition, in CBPV.ProgramContexts]
cctx_ind_2 [definition, in CBPV.ProgramContexts]
cctxᵥ [inductive, in CBPV.CBV.DenotationalSemantics]
cctxᵥAppL [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥAppR [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥCasePC [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥCasePV [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥCaseSL [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥCaseSR [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥCaseSV [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥHole [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTyping [inductive, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingAppL [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingAppR [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCasePC [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCasePV [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCaseSL [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCaseSR [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCaseSV [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingHole [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingVctx [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥVctx [constructor, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_cctx_comp [definition, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_cctx_value [definition, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_comp_typing_soundness [definition, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_value_typing_soundness [definition, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_typing_ind_3 [definition, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_typing_ind_2 [definition, in CBPV.CBV.DenotationalSemantics]
cctxᵥ_ind_2 [definition, in CBPV.CBV.DenotationalSemantics]
church_rosser [lemma, in CBPV.AbstractReductionSystems]
close [inductive, in CBPV.StrongNormalisation]
ClosedSemanticSoundness [lemma, in CBPV.SemanticTyping]
closev [inductive, in CBPV.StrongNormalisation]
closev_ren [lemma, in CBPV.StrongNormalisation]
closev_base [lemma, in CBPV.StrongNormalisation]
closev_V [constructor, in CBPV.StrongNormalisation]
closev_var [constructor, in CBPV.StrongNormalisation]
close_ren [lemma, in CBPV.StrongNormalisation]
close_base [lemma, in CBPV.StrongNormalisation]
close_red [lemma, in CBPV.StrongNormalisation]
close_sn [lemma, in CBPV.StrongNormalisation]
close_step [constructor, in CBPV.StrongNormalisation]
ClosureRelations [section, in CBPV.AbstractReductionSystems]
ClosureRelations.R [variable, in CBPV.AbstractReductionSystems]
ClosureRelations.X [variable, in CBPV.AbstractReductionSystems]
closure_under_reduction [lemma, in CBPV.LogicalEquivalence]
closure_under_expansion [lemma, in CBPV.LogicalEquivalence]
closure_ctx_red [lemma, in CBPV.DenotationalSemantics]
closure_ctx_eqv [lemma, in CBPV.DenotationalSemantics]
closure_under_expansion [lemma, in CBPV.SemanticTyping]
CommaNotation [module, in CBPV.fintype]
_ , _ (subst_scope) [notation, in CBPV.fintype]
commute_caseS_lambda [lemma, in CBPV.EquationalTheory]
commute_let_app [lemma, in CBPV.EquationalTheory]
commute_let_tuple [lemma, in CBPV.EquationalTheory]
commute_let_lam [lemma, in CBPV.EquationalTheory]
commute_let_let [lemma, in CBPV.EquationalTheory]
comp [inductive, in CBPV.Syntax]
comp [definition, in CBPV.fintype]
CompatibilityLemmas [section, in CBPV.LogicalEquivalence]
CompatibilityLemmas [section, in CBPV.StrongNormalisation]
CompatibilityLemmas.A [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.A [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.A1 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.A1 [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.A2 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.A2 [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.B [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.B [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.B1 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.B1 [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.B2 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.B2 [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.c1 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c1' [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c2 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c2' [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c3 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c4 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c5 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c6 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c7 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.c8 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.n [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.n [variable, in CBPV.StrongNormalisation]
CompatibilityLemmas.v1 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.v1' [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.v2 [variable, in CBPV.LogicalEquivalence]
CompatibilityLemmas.v2' [variable, in CBPV.LogicalEquivalence]
compatibility_lemmas.B2 [variable, in CBPV.SemanticTyping]
compatibility_lemmas.B1 [variable, in CBPV.SemanticTyping]
compatibility_lemmas.B [variable, in CBPV.SemanticTyping]
compatibility_lemmas.A2 [variable, in CBPV.SemanticTyping]
compatibility_lemmas.A1 [variable, in CBPV.SemanticTyping]
compatibility_lemmas.A [variable, in CBPV.SemanticTyping]
compatibility_lemmas.Gamma [variable, in CBPV.SemanticTyping]
compatibility_lemmas.n [variable, in CBPV.SemanticTyping]
compatibility_lemmas [section, in CBPV.SemanticTyping]
compat_caseP [lemma, in CBPV.SemanticTyping]
compat_caseS [lemma, in CBPV.SemanticTyping]
compat_caseZ [lemma, in CBPV.SemanticTyping]
compat_force [lemma, in CBPV.SemanticTyping]
compat_proj [lemma, in CBPV.SemanticTyping]
compat_tuple [lemma, in CBPV.SemanticTyping]
compat_app [lemma, in CBPV.SemanticTyping]
compat_ret [lemma, in CBPV.SemanticTyping]
compat_letin [lemma, in CBPV.SemanticTyping]
compat_lambda [lemma, in CBPV.SemanticTyping]
compat_cone [lemma, in CBPV.SemanticTyping]
compat_thunk [lemma, in CBPV.SemanticTyping]
compat_sum [lemma, in CBPV.SemanticTyping]
compat_pair [lemma, in CBPV.SemanticTyping]
compat_unit [lemma, in CBPV.SemanticTyping]
compat_var [lemma, in CBPV.SemanticTyping]
compat_caseP [lemma, in CBPV.StrongNormalisation]
compat_caseS [lemma, in CBPV.StrongNormalisation]
compat_caseZ [lemma, in CBPV.StrongNormalisation]
compat_force [lemma, in CBPV.StrongNormalisation]
compat_proj [lemma, in CBPV.StrongNormalisation]
compat_tuple [lemma, in CBPV.StrongNormalisation]
compat_app [lemma, in CBPV.StrongNormalisation]
compat_ret [lemma, in CBPV.StrongNormalisation]
compat_letin [lemma, in CBPV.StrongNormalisation]
compat_lambda [lemma, in CBPV.StrongNormalisation]
compat_cone [lemma, in CBPV.StrongNormalisation]
compat_thunk [lemma, in CBPV.StrongNormalisation]
compat_sum [lemma, in CBPV.StrongNormalisation]
compat_pair [lemma, in CBPV.StrongNormalisation]
compat_unit [lemma, in CBPV.StrongNormalisation]
compat_var [lemma, in CBPV.StrongNormalisation]
compat_caseP_E [lemma, in CBPV.StrongNormalisation]
compat_caseS_E [lemma, in CBPV.StrongNormalisation]
compat_caseZ_E [lemma, in CBPV.StrongNormalisation]
compat_force_E [lemma, in CBPV.StrongNormalisation]
compat_proj_E [lemma, in CBPV.StrongNormalisation]
compat_tuple_E [lemma, in CBPV.StrongNormalisation]
compat_app_E [lemma, in CBPV.StrongNormalisation]
compat_ret_E [lemma, in CBPV.StrongNormalisation]
compat_letin_E [lemma, in CBPV.StrongNormalisation]
compat_lambda_E [lemma, in CBPV.StrongNormalisation]
compat_thunk_E [lemma, in CBPV.StrongNormalisation]
compat_sum_E [lemma, in CBPV.StrongNormalisation]
compat_pair_E [lemma, in CBPV.StrongNormalisation]
compComp_comp [lemma, in CBPV.Syntax]
compComp_value [lemma, in CBPV.Syntax]
compComp_exp [lemma, in CBPV.CBN.CBN]
compComp_Exp [lemma, in CBPV.CBV.CBV]
compComp_Value [lemma, in CBPV.CBV.CBV]
compComp'_comp [lemma, in CBPV.Syntax]
compComp'_value [lemma, in CBPV.Syntax]
compComp'_exp [lemma, in CBPV.CBN.CBN]
compComp'_Exp [lemma, in CBPV.CBV.CBV]
compComp'_Value [lemma, in CBPV.CBV.CBV]
compRenRen_comp [definition, in CBPV.Syntax]
compRenRen_value [definition, in CBPV.Syntax]
compRenRen_exp [definition, in CBPV.CBN.CBN]
compRenRen_Exp [definition, in CBPV.CBV.CBV]
compRenRen_Value [definition, in CBPV.CBV.CBV]
compRenSubst_comp [definition, in CBPV.Syntax]
compRenSubst_value [definition, in CBPV.Syntax]
compRenSubst_exp [definition, in CBPV.CBN.CBN]
compRenSubst_Exp [definition, in CBPV.CBV.CBV]
compRenSubst_Value [definition, in CBPV.CBV.CBV]
compRen_comp [lemma, in CBPV.Syntax]
compRen_value [lemma, in CBPV.Syntax]
compRen_exp [lemma, in CBPV.CBN.CBN]
compRen_Exp [lemma, in CBPV.CBV.CBV]
compRen_Value [lemma, in CBPV.CBV.CBV]
compRen'_comp [lemma, in CBPV.Syntax]
compRen'_value [lemma, in CBPV.Syntax]
compRen'_exp [lemma, in CBPV.CBN.CBN]
compRen'_Exp [lemma, in CBPV.CBV.CBV]
compRen'_Value [lemma, in CBPV.CBV.CBV]
compSubstRen__comp [definition, in CBPV.Syntax]
compSubstRen__value [definition, in CBPV.Syntax]
compSubstRen__exp [definition, in CBPV.CBN.CBN]
compSubstRen__Exp [definition, in CBPV.CBV.CBV]
compSubstRen__Value [definition, in CBPV.CBV.CBV]
compSubstSubst_comp [definition, in CBPV.Syntax]
compSubstSubst_value [definition, in CBPV.Syntax]
compSubstSubst_exp [definition, in CBPV.CBN.CBN]
compSubstSubst_Exp [definition, in CBPV.CBV.CBV]
compSubstSubst_Value [definition, in CBPV.CBV.CBV]
comptype [inductive, in CBPV.Syntax]
comptype [inductive, in CBPV.Terms]
comptypeif [definition, in CBPV.ProgramContexts]
comptype_ind_2 [definition, in CBPV.Terms]
computation_typing_ind_4 [definition, in CBPV.SyntacticTyping]
computation_typing_ind_3 [definition, in CBPV.SyntacticTyping]
computation_typing_ind_2 [definition, in CBPV.SyntacticTyping]
computation_typing [inductive, in CBPV.SyntacticTyping]
computation_typing_ext [lemma, in CBPV.CBN.CBN_CBPV]
comp_semeq_trans [instance, in CBPV.LogicalEquivalence]
comp_semeq_transitive [lemma, in CBPV.LogicalEquivalence]
comp_semeq_symm [instance, in CBPV.LogicalEquivalence]
comp_semeq_symmetry [lemma, in CBPV.LogicalEquivalence]
comp_semeq [definition, in CBPV.LogicalEquivalence]
comp_evaluates [lemma, in CBPV.SemanticTyping]
comp_nf [lemma, in CBPV.SemanticTyping]
comp_semtype [definition, in CBPV.SemanticTyping]
comp_typepres_substitution [definition, in CBPV.SyntacticTyping]
comp_typepres_renaming [definition, in CBPV.SyntacticTyping]
comp_semtype [definition, in CBPV.StrongNormalisation]
comp_ind_2 [definition, in CBPV.Terms]
comp_obseq_cctx_congruence [lemma, in CBPV.ObservationalEquivalence]
comp_obseq_vctx_congruence [lemma, in CBPV.ObservationalEquivalence]
comp_obseq [definition, in CBPV.ObservationalEquivalence]
cone [constructor, in CBPV.Syntax]
cone [constructor, in CBPV.Terms]
confluence [lemma, in CBPV.CBN.strongStory]
Confluence [section, in CBPV.AbstractReductionSystems]
confluence [lemma, in CBPV.Confluence]
Confluence [library]
confluence_steps [lemma, in CBPV.Semantics]
confluence_unique_normal_forms [lemma, in CBPV.AbstractReductionSystems]
confluence_normal_right [lemma, in CBPV.AbstractReductionSystems]
confluence_normal_left [lemma, in CBPV.AbstractReductionSystems]
Confluence.X [variable, in CBPV.AbstractReductionSystems]
confluent [definition, in CBPV.AbstractReductionSystems]
confluent_semi [lemma, in CBPV.AbstractReductionSystems]
congruence_caseP [lemma, in CBPV.LogicalEquivalence]
congruence_caseS [lemma, in CBPV.LogicalEquivalence]
congruence_caseZ [lemma, in CBPV.LogicalEquivalence]
congruence_proj [lemma, in CBPV.LogicalEquivalence]
congruence_eagerlet [lemma, in CBPV.LogicalEquivalence]
congruence_letin [lemma, in CBPV.LogicalEquivalence]
congruence_ret [lemma, in CBPV.LogicalEquivalence]
congruence_tuple [lemma, in CBPV.LogicalEquivalence]
congruence_app [lemma, in CBPV.LogicalEquivalence]
congruence_lambda [lemma, in CBPV.LogicalEquivalence]
congruence_force [lemma, in CBPV.LogicalEquivalence]
congruence_cu [lemma, in CBPV.LogicalEquivalence]
congruence_thunk [lemma, in CBPV.LogicalEquivalence]
congruence_inj [lemma, in CBPV.LogicalEquivalence]
congruence_pair [lemma, in CBPV.LogicalEquivalence]
congruence_u [lemma, in CBPV.LogicalEquivalence]
congr_caseP [lemma, in CBPV.Syntax]
congr_caseS [lemma, in CBPV.Syntax]
congr_caseZ [lemma, in CBPV.Syntax]
congr_proj [lemma, in CBPV.Syntax]
congr_letin [lemma, in CBPV.Syntax]
congr_ret [lemma, in CBPV.Syntax]
congr_tuple [lemma, in CBPV.Syntax]
congr_app [lemma, in CBPV.Syntax]
congr_lambda [lemma, in CBPV.Syntax]
congr_force [lemma, in CBPV.Syntax]
congr_cu [lemma, in CBPV.Syntax]
congr_thunk [lemma, in CBPV.Syntax]
congr_inj [lemma, in CBPV.Syntax]
congr_pair [lemma, in CBPV.Syntax]
congr_u [lemma, in CBPV.Syntax]
congr_arrow [lemma, in CBPV.Syntax]
congr_Pi [lemma, in CBPV.Syntax]
congr_F [lemma, in CBPV.Syntax]
congr_cone [lemma, in CBPV.Syntax]
congr_cross [lemma, in CBPV.Syntax]
congr_Sigma [lemma, in CBPV.Syntax]
congr_U [lemma, in CBPV.Syntax]
congr_one [lemma, in CBPV.Syntax]
congr_zero [lemma, in CBPV.Syntax]
congr_CaseS [lemma, in CBPV.CBN.CBN]
congr_Inj [lemma, in CBPV.CBN.CBN]
congr_Proj [lemma, in CBPV.CBN.CBN]
congr_Pair [lemma, in CBPV.CBN.CBN]
congr_App [lemma, in CBPV.CBN.CBN]
congr_Lam [lemma, in CBPV.CBN.CBN]
congr_One [lemma, in CBPV.CBN.CBN]
congr_Plus [lemma, in CBPV.CBN.CBN]
congr_Cross [lemma, in CBPV.CBN.CBN]
congr_Arr [lemma, in CBPV.CBN.CBN]
congr_Unit [lemma, in CBPV.CBN.CBN]
congr_CaseP [lemma, in CBPV.CBV.CBV]
congr_CaseS [lemma, in CBPV.CBV.CBV]
congr_App [lemma, in CBPV.CBV.CBV]
congr_Val [lemma, in CBPV.CBV.CBV]
congr_Inj [lemma, in CBPV.CBV.CBV]
congr_Pair [lemma, in CBPV.CBV.CBV]
congr_Lam [lemma, in CBPV.CBV.CBV]
congr_One [lemma, in CBPV.CBV.CBV]
congr_Plus [lemma, in CBPV.CBV.CBV]
congr_Cross [lemma, in CBPV.CBV.CBV]
congr_Arr [lemma, in CBPV.CBV.CBV]
congr_Unit [lemma, in CBPV.CBV.CBV]
cons_twice_ctx_subst [lemma, in CBPV.DenotationalSemantics]
cons_ctx_subst [lemma, in CBPV.DenotationalSemantics]
contextStep [constructor, in CBPV.Semantics]
context_typing_decomposition_cctx_comp [definition, in CBPV.ProgramContexts]
context_typing_decomposition_cctx_value [definition, in CBPV.ProgramContexts]
context_typing_decomposition_vctx_comp [definition, in CBPV.ProgramContexts]
context_typing_decomposition_vctx_value [definition, in CBPV.ProgramContexts]
counted [inductive, in CBPV.AbstractReductionSystems]
countedRefl [constructor, in CBPV.AbstractReductionSystems]
countedStep [constructor, in CBPV.AbstractReductionSystems]
counted_exp [lemma, in CBPV.AbstractReductionSystems]
counted_trans [lemma, in CBPV.AbstractReductionSystems]
Counterexample [module, in CBPV.CBV.strongStory]
Counterexample.e [variable, in CBPV.CBV.strongStory]
Counterexample.M [variable, in CBPV.CBV.strongStory]
Counterexample.M' [variable, in CBPV.CBV.strongStory]
Counterexample.normal_e [lemma, in CBPV.CBV.strongStory]
Counterexample.not_normal_e [lemma, in CBPV.CBV.strongStory]
Counterexample.step1 [lemma, in CBPV.CBV.strongStory]
Counterexample.step2 [lemma, in CBPV.CBV.strongStory]
cross [constructor, in CBPV.Syntax]
cross [constructor, in CBPV.Terms]
Cross [constructor, in CBPV.CBN.CBN]
Cross [constructor, in CBPV.CBV.CBV]
cstep [inductive, in CBPV.Semantics]
ctx [definition, in CBPV.SyntacticTyping]
ctx_cbv [definition, in CBPV.CBV.CBV_CBPV]
ctx_plus [lemma, in CBPV.Eagerlet]
ctx_plus_value [lemma, in CBPV.CBV.strongStory]
ctx_plus [lemma, in CBPV.CBV.strongStory]
cu [constructor, in CBPV.Syntax]
C_trans [instance, in CBPV.LogicalEquivalence]
C_symm [instance, in CBPV.LogicalEquivalence]
D
Denotation [section, in CBPV.CBN.DenotationalSemantics]Denotation [section, in CBPV.CBV.DenotationalSemantics]
DenotationalSemantics [section, in CBPV.DenotationalSemantics]
DenotationalSemantics [library]
DenotationalSemantics [library]
DenotationalSemantics [library]
DenotationalSemantics.T [variable, in CBPV.DenotationalSemantics]
denotation_context [lemma, in CBPV.DenotationalSemantics]
denotation_of_groundtypes_inhabited [lemma, in CBPV.DenotationalSemantics]
denotation_termination [lemma, in CBPV.Termination]
Denotation.A [variable, in CBPV.CBV.DenotationalSemantics]
Denotation.Gamma [variable, in CBPV.CBV.DenotationalSemantics]
Denotation.mono_requirement [variable, in CBPV.CBN.DenotationalSemantics]
Denotation.mono_requirement [variable, in CBPV.CBV.DenotationalSemantics]
Denotation.n [variable, in CBPV.CBV.DenotationalSemantics]
Denotation.T [variable, in CBPV.CBN.DenotationalSemantics]
Denotation.T [variable, in CBPV.CBV.DenotationalSemantics]
denote_comptyping [definition, in CBPV.DenotationalSemantics]
denote_valtyping [definition, in CBPV.DenotationalSemantics]
denote_context [definition, in CBPV.DenotationalSemantics]
denote_comptype [definition, in CBPV.DenotationalSemantics]
denote_valtype [definition, in CBPV.DenotationalSemantics]
denote_cbn_ctx [definition, in CBPV.CBN.DenotationalSemantics]
denote_exp [definition, in CBPV.CBN.DenotationalSemantics]
denote_type [definition, in CBPV.CBN.DenotationalSemantics]
denote_cbv_ctx [definition, in CBPV.CBV.DenotationalSemantics]
denote_val [definition, in CBPV.CBV.DenotationalSemantics]
denote_exp [definition, in CBPV.CBV.DenotationalSemantics]
denote_type [definition, in CBPV.CBV.DenotationalSemantics]
destruct_comp_obseq [lemma, in CBPV.ObservationalEquivalence]
destruct_value_obseq [lemma, in CBPV.ObservationalEquivalence]
diamond [definition, in CBPV.AbstractReductionSystems]
diamond_ext [lemma, in CBPV.AbstractReductionSystems]
diamond_confluent [lemma, in CBPV.AbstractReductionSystems]
diamond_semi_confluent [lemma, in CBPV.AbstractReductionSystems]
E
E [abbreviation, in CBPV.LogicalEquivalence]E [abbreviation, in CBPV.SemanticTyping]
E [abbreviation, in CBPV.StrongNormalisation]
eagerlet [definition, in CBPV.Eagerlet]
Eagerlet [library]
eagerlet_substcomp [lemma, in CBPV.Eagerlet]
eagerlet_rencomp [lemma, in CBPV.Eagerlet]
eagerlet_ty [lemma, in CBPV.Eagerlet]
eagerlet_inv [lemma, in CBPV.Eagerlet]
ectx [inductive, in CBPV.Semantics]
ectx [inductive, in CBPV.CBN.DenotationalSemantics]
ectxApp [constructor, in CBPV.Semantics]
ectxAppL [constructor, in CBPV.CBN.DenotationalSemantics]
ectxAppR [constructor, in CBPV.CBN.DenotationalSemantics]
ectxCaseSL [constructor, in CBPV.CBN.DenotationalSemantics]
ectxCaseSR [constructor, in CBPV.CBN.DenotationalSemantics]
ectxCaseSV [constructor, in CBPV.CBN.DenotationalSemantics]
ectxHole [constructor, in CBPV.Semantics]
ectxHole [constructor, in CBPV.CBN.DenotationalSemantics]
ectxInj [constructor, in CBPV.CBN.DenotationalSemantics]
ectxLambda [constructor, in CBPV.CBN.DenotationalSemantics]
ectxLetin [constructor, in CBPV.Semantics]
ectxPairL [constructor, in CBPV.CBN.DenotationalSemantics]
ectxPairR [constructor, in CBPV.CBN.DenotationalSemantics]
ectxProj [constructor, in CBPV.Semantics]
ectxProj [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTyping [inductive, in CBPV.CBN.DenotationalSemantics]
ectxTypingAppL [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingAppR [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingCaseSL [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingCaseSR [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingCaseSV [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingHole [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingInj [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingLambda [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingPairL [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingPairR [constructor, in CBPV.CBN.DenotationalSemantics]
ectxTypingProj [constructor, in CBPV.CBN.DenotationalSemantics]
ectx_compose [lemma, in CBPV.Semantics]
ectx_decompose [lemma, in CBPV.Semantics]
ectx_cctx_typing [lemma, in CBPV.CBN.DenotationalSemantics]
ectx_cctx [lemma, in CBPV.CBN.DenotationalSemantics]
ectx_typing_soundness [definition, in CBPV.CBN.DenotationalSemantics]
EquationalTheory [library]
Equiv [definition, in CBPV.EquationalTheory]
equiv [definition, in CBPV.AbstractReductionSystems]
EquivCBN [definition, in CBPV.EquationalTheory]
EquivCBV [definition, in CBPV.EquationalTheory]
EquivCBVᵥ [definition, in CBPV.EquationalTheory]
equiv_soundness_CBVᵥ [lemma, in CBPV.EquationalTheory]
equiv_soundness_CBV [lemma, in CBPV.EquationalTheory]
equiv_soundness_CBN [lemma, in CBPV.EquationalTheory]
equiv_soundness_CBPVᵥ [lemma, in CBPV.EquationalTheory]
equiv_soundness_CBPV [lemma, in CBPV.EquationalTheory]
equiv_translation_CBVᵥ [lemma, in CBPV.EquationalTheory]
equiv_translation_CBV [lemma, in CBPV.EquationalTheory]
equiv_translation_CBN [lemma, in CBPV.EquationalTheory]
equiv_exp_obseq [instance, in CBPV.CBN.DenotationalSemantics]
equiv_comp_obseq [instance, in CBPV.ObservationalEquivalence]
equiv_value_obseq [instance, in CBPV.ObservationalEquivalence]
equiv_Equivalence [instance, in CBPV.AbstractReductionSystems]
equiv_star [lemma, in CBPV.AbstractReductionSystems]
equiv_symm [lemma, in CBPV.AbstractReductionSystems]
equiv_trans [lemma, in CBPV.AbstractReductionSystems]
equiv_value_obseq [instance, in CBPV.CBV.DenotationalSemantics]
equiv_exp_obseq [instance, in CBPV.CBV.DenotationalSemantics]
Equivᵥ [definition, in CBPV.EquationalTheory]
eta_caseP [lemma, in CBPV.EquationalTheory]
eta_caseS [lemma, in CBPV.EquationalTheory]
eta_pair [lemma, in CBPV.EquationalTheory]
eta_lambda [lemma, in CBPV.EquationalTheory]
eta_let [lemma, in CBPV.EquationalTheory]
eta_thunk [lemma, in CBPV.EquationalTheory]
eta_if'_typed [lemma, in CBPV.CBN.DenotationalSemantics]
eta_if_typed [lemma, in CBPV.CBN.DenotationalSemantics]
eta_if' [definition, in CBPV.CBN.DenotationalSemantics]
eta_if [definition, in CBPV.CBN.DenotationalSemantics]
eval [definition, in CBPV.Semantics]
eval [definition, in CBPV.CBN.CBN_CBPV]
evaluates [definition, in CBPV.AbstractReductionSystems]
evaluates_backwards [lemma, in CBPV.CBN.strongStory]
evaluates_forward [lemma, in CBPV.CBN.strongStory]
evaluates_to [lemma, in CBPV.CBN.weakStory]
eval_exp [definition, in CBPV.CBV.CBV_CBPV]
eval_val [definition, in CBPV.CBV.CBV_CBPV]
eval_ty [definition, in CBPV.CBV.CBV_CBPV]
eval_evaluates [lemma, in CBPV.Semantics]
eval_bigstep [lemma, in CBPV.Semantics]
eval_eval'_true [lemma, in CBPV.CBN.DenotationalSemantics]
eval_eval' [lemma, in CBPV.CBN.DenotationalSemantics]
eval_CBN [definition, in CBPV.CBN.DenotationalSemantics]
eval_ectx [definition, in CBPV.CBN.DenotationalSemantics]
eval_subst_up_value_value [lemma, in CBPV.CBN.CBN_CBPV]
evaL_subst_ren [lemma, in CBPV.CBN.CBN_CBPV]
eval_subst_cons [lemma, in CBPV.CBN.CBN_CBPV]
eval_subst [definition, in CBPV.CBN.CBN_CBPV]
eval_ctx_cons [lemma, in CBPV.CBN.CBN_CBPV]
eval_ctx [definition, in CBPV.CBN.CBN_CBPV]
eval_ty [definition, in CBPV.CBN.CBN_CBPV]
eval_eval'_tt [lemma, in CBPV.CBV.DenotationalSemantics]
eval_CBVᵥ [definition, in CBPV.CBV.DenotationalSemantics]
eval_CBV [definition, in CBPV.CBV.DenotationalSemantics]
eval_eval' [lemma, in CBPV.CBV.DenotationalSemantics]
eval_ctx_cons [lemma, in CBPV.CBV.DenotationalSemantics]
eval' [definition, in CBPV.CBN.DenotationalSemantics]
eval'_vctx_comp_typing [definition, in CBPV.CBV.DenotationalSemantics]
eval'_vctx_value_typing [definition, in CBPV.CBV.DenotationalSemantics]
eval'_cctx_comp_typing [definition, in CBPV.CBV.DenotationalSemantics]
eval'_cctx_value_typing [definition, in CBPV.CBV.DenotationalSemantics]
eval'_cctx [definition, in CBPV.CBV.DenotationalSemantics]
eval'_vctx [definition, in CBPV.CBV.DenotationalSemantics]
eval'_exp [definition, in CBPV.CBV.DenotationalSemantics]
eval'_val [definition, in CBPV.CBV.DenotationalSemantics]
exp [inductive, in CBPV.CBN.CBN]
Exp [inductive, in CBPV.CBV.CBV]
exponential_t_algebra [definition, in CBPV.DenotationalSemantics]
ExpVal_ind [definition, in CBPV.CBV.CBV_CBPV]
Exp_ind_2 [definition, in CBPV.CBV.CBV_CBPV]
exp_obseq [definition, in CBPV.CBN.DenotationalSemantics]
exp_value_ind_2 [definition, in CBPV.CBV.strongStory]
exp_obseq [definition, in CBPV.CBV.DenotationalSemantics]
extend [definition, in CBPV.DenotationalSemantics]
extend' [definition, in CBPV.DenotationalSemantics]
extRen_comp [definition, in CBPV.Syntax]
extRen_value [definition, in CBPV.Syntax]
extRen_exp [definition, in CBPV.CBN.CBN]
extRen_Exp [definition, in CBPV.CBV.CBV]
extRen_Value [definition, in CBPV.CBV.CBV]
ext_comp [definition, in CBPV.Syntax]
ext_value [definition, in CBPV.Syntax]
ext_exp [definition, in CBPV.CBN.CBN]
ext_Exp [definition, in CBPV.CBV.CBV]
ext_Value [definition, in CBPV.CBV.CBV]
E_trans [instance, in CBPV.LogicalEquivalence]
E_transitive [lemma, in CBPV.LogicalEquivalence]
E_symm [instance, in CBPV.LogicalEquivalence]
E_symmetry [lemma, in CBPV.LogicalEquivalence]
E_ind2 [lemma, in CBPV.StrongNormalisation]
E_ind [lemma, in CBPV.StrongNormalisation]
E_ren [lemma, in CBPV.StrongNormalisation]
E' [definition, in CBPV.LogicalEquivalence]
E' [definition, in CBPV.SemanticTyping]
F
F [constructor, in CBPV.Syntax]F [constructor, in CBPV.Terms]
ff [definition, in CBPV.CBN.DenotationalSemantics]
ff [definition, in CBPV.CBV.DenotationalSemantics]
fill [definition, in CBPV.Semantics]
fillc [definition, in CBPV.ProgramContexts]
fillcᵥ [definition, in CBPV.CBV.DenotationalSemantics]
fille [definition, in CBPV.CBN.DenotationalSemantics]
fillv [definition, in CBPV.ProgramContexts]
fillvᵥ [definition, in CBPV.CBV.DenotationalSemantics]
fin [definition, in CBPV.fintype]
fintype [library]
fmap [definition, in CBPV.DenotationalSemantics]
fmap_funct [lemma, in CBPV.DenotationalSemantics]
force [constructor, in CBPV.Syntax]
forward_simulation [lemma, in CBPV.CBV.weakStory]
free_t_algebra [definition, in CBPV.DenotationalSemantics]
funcomp [definition, in CBPV.fintype]
functional [definition, in CBPV.AbstractReductionSystems]
fundamental_property_comp [lemma, in CBPV.LogicalEquivalence]
fundamental_property_value [lemma, in CBPV.LogicalEquivalence]
fundamental_property [lemma, in CBPV.LogicalEquivalence]
G
G [definition, in CBPV.LogicalEquivalence]G [definition, in CBPV.SemanticTyping]
G [definition, in CBPV.StrongNormalisation]
gbool [definition, in CBPV.CBN.DenotationalSemantics]
gbool [definition, in CBPV.CBV.DenotationalSemantics]
gcross [constructor, in CBPV.Terms]
gone [constructor, in CBPV.Terms]
groundtype [inductive, in CBPV.Terms]
groundtypes_are_simple [lemma, in CBPV.LogicalEquivalence]
ground_equiv [lemma, in CBPV.DenotationalSemantics]
gsum [constructor, in CBPV.Terms]
G_cons [lemma, in CBPV.LogicalEquivalence]
G_trans [instance, in CBPV.LogicalEquivalence]
G_transitive [lemma, in CBPV.LogicalEquivalence]
G_symm [instance, in CBPV.LogicalEquivalence]
G_symmetry [lemma, in CBPV.LogicalEquivalence]
G_ext [lemma, in CBPV.StrongNormalisation]
G_ren [lemma, in CBPV.StrongNormalisation]
G_scons [lemma, in CBPV.StrongNormalisation]
G_id [lemma, in CBPV.StrongNormalisation]
H
has_typeE [inductive, in CBPV.CBV.CBV_CBPV]has_typeV [inductive, in CBPV.CBV.CBV_CBPV]
has_type_ind [definition, in CBPV.CBV.DenotationalSemantics]
has_typeE_2 [definition, in CBPV.CBV.DenotationalSemantics]
has_typeV_2 [definition, in CBPV.CBV.DenotationalSemantics]
I
id [definition, in CBPV.fintype]IdMonad [definition, in CBPV.DenotationalSemantics]
idren [definition, in CBPV.fintype]
ids [projection, in CBPV.fintype]
ids [constructor, in CBPV.fintype]
idSubst_comp [definition, in CBPV.Syntax]
idSubst_value [definition, in CBPV.Syntax]
idSubst_exp [definition, in CBPV.CBN.CBN]
idSubst_Exp [definition, in CBPV.CBV.CBV]
idSubst_Value [definition, in CBPV.CBV.CBV]
inhab [inductive, in CBPV.Base]
inhabited [constructor, in CBPV.Base]
inj [constructor, in CBPV.Syntax]
Inj [constructor, in CBPV.CBN.CBN]
Inj [constructor, in CBPV.CBV.CBV]
injective [abbreviation, in CBPV.CBN.CBN_CBPV]
injective_eval [lemma, in CBPV.CBV.CBV_CBPV]
injective_renup [lemma, in CBPV.CBV.CBV_CBPV]
injective_shift [lemma, in CBPV.CBV.CBV_CBPV]
injective_eval [lemma, in CBPV.CBN.CBN_CBPV]
inj_star_inv [lemma, in CBPV.StrongReduction]
instId_comp [lemma, in CBPV.Syntax]
instId_value [lemma, in CBPV.Syntax]
instId_exp [lemma, in CBPV.CBN.CBN]
instId_Exp [lemma, in CBPV.CBV.CBV]
instId_Value [lemma, in CBPV.CBV.CBV]
it [definition, in CBPV.Base]
Iter [section, in CBPV.Base]
Iter.f [variable, in CBPV.Base]
Iter.X [variable, in CBPV.Base]
it_shift [lemma, in CBPV.Base]
J
joinable [definition, in CBPV.AbstractReductionSystems]joinable_ext [lemma, in CBPV.AbstractReductionSystems]
K
K [definition, in CBPV.CBN.DenotationalSemantics]K_filled_typed [lemma, in CBPV.CBN.DenotationalSemantics]
K_typed [lemma, in CBPV.CBN.DenotationalSemantics]
L
Lam [constructor, in CBPV.CBN.CBN]Lam [constructor, in CBPV.CBV.CBV]
lambda [constructor, in CBPV.Syntax]
letin [constructor, in CBPV.Syntax]
let_to_eagerlet [lemma, in CBPV.Eagerlet]
LogicalEquivalence [library]
LogicalRelation [section, in CBPV.DenotationalSemantics]
LogicalRelation.mono_requirement [variable, in CBPV.DenotationalSemantics]
LogicalRelation.T [variable, in CBPV.DenotationalSemantics]
logical_equivalence_strong_reduction_value_steps [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_strong_reduction_steps [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_weak_reduction_steps [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_strong_reduction_value [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_strong_reduction [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_weak_reduction [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_primitive_reduction [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_obseq [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_congruent_cctx_comp [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_congruent_cctx_value [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_congruent_vctx_comp [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_congruent_vctx_value [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_congruent [lemma, in CBPV.LogicalEquivalence]
logical_equivalence_Equivᵥ [lemma, in CBPV.EquationalTheory]
logical_equivalence_Equiv [lemma, in CBPV.EquationalTheory]
M
mbind [projection, in CBPV.DenotationalSemantics]mkCBN [constructor, in CBPV.CBN.DenotationalSemantics]
mkCBPVc [constructor, in CBPV.ObservationalEquivalence]
mkCBPVv [constructor, in CBPV.ObservationalEquivalence]
mkCBV [constructor, in CBPV.CBV.DenotationalSemantics]
mkCBVᵥ [constructor, in CBPV.CBV.DenotationalSemantics]
Monad [record, in CBPV.DenotationalSemantics]
monad1 [projection, in CBPV.DenotationalSemantics]
monad2 [projection, in CBPV.DenotationalSemantics]
monad3 [projection, in CBPV.DenotationalSemantics]
morphism [definition, in CBPV.AbstractReductionSystems]
mreturn [projection, in CBPV.DenotationalSemantics]
MStep_preserved [lemma, in CBPV.CBV.strongStory]
MStep_preserved [lemma, in CBPV.CBV.weakStory]
mu [definition, in CBPV.DenotationalSemantics]
mutindt_vctx_cctx_typing [definition, in CBPV.ProgramContexts]
mutindt_value_computation_typing [definition, in CBPV.SyntacticTyping]
mutindt_vctxᵥ_cctxᵥ_typing [definition, in CBPV.CBV.DenotationalSemantics]
mutind_vctx_cctx_typing [definition, in CBPV.ProgramContexts]
mutind_vctx_cctx [definition, in CBPV.ProgramContexts]
mutind_value_computation_typing [definition, in CBPV.SyntacticTyping]
mutind_value_exp [definition, in CBPV.CBV.strongStory]
mutind_valtype_comptype [definition, in CBPV.Terms]
mutind_val_comp [definition, in CBPV.Terms]
mutind_parstep [definition, in CBPV.Confluence]
mutind_vctxᵥ_cctxᵥ_typing [definition, in CBPV.CBV.DenotationalSemantics]
mutind_cbv_ctx [definition, in CBPV.CBV.DenotationalSemantics]
mutind_sstep [definition, in CBPV.StrongReduction]
mu_fmap [lemma, in CBPV.DenotationalSemantics]
N
nat_to_fin [definition, in CBPV.Terms]nf [inductive, in CBPV.Semantics]
nfCu [constructor, in CBPV.Semantics]
nfLam [constructor, in CBPV.Semantics]
nfRet [constructor, in CBPV.Semantics]
nfTup [constructor, in CBPV.Semantics]
nf_normal [lemma, in CBPV.Semantics]
Normal [definition, in CBPV.AbstractReductionSystems]
normalizing_extension [lemma, in CBPV.Semantics]
Normal_preserved' [lemma, in CBPV.CBN.weakStory]
Normal_preserved [lemma, in CBPV.CBN.weakStory]
Normal_nf [lemma, in CBPV.SemanticTyping]
normal_bigstep [lemma, in CBPV.Semantics]
normal_tt [lemma, in CBPV.CBN.DenotationalSemantics]
Normal_preserved [lemma, in CBPV.CBV.weakStory]
Normal_star_stops [lemma, in CBPV.AbstractReductionSystems]
Normal_SN [lemma, in CBPV.AbstractReductionSystems]
null [definition, in CBPV.fintype]
O
obseq_contains_steps [lemma, in CBPV.LogicalEquivalence]obseq_contains_step [lemma, in CBPV.LogicalEquivalence]
obseq_contains_pstep [lemma, in CBPV.LogicalEquivalence]
obseq_soundness [lemma, in CBPV.CBN.DenotationalSemantics]
obseq_soundness' [lemma, in CBPV.CBN.DenotationalSemantics]
obseq_soundnessᵥ [lemma, in CBPV.CBV.DenotationalSemantics]
obseq_soundness [lemma, in CBPV.CBV.DenotationalSemantics]
obseq_soundnessᵥ' [lemma, in CBPV.CBV.DenotationalSemantics]
obseq_soundness' [lemma, in CBPV.CBV.DenotationalSemantics]
ObservationalEquivalence [library]
ObservationalEquivalenceSoundness [section, in CBPV.CBN.DenotationalSemantics]
ObservationalEquivalenceSoundness [section, in CBPV.CBV.DenotationalSemantics]
one [constructor, in CBPV.Syntax]
one [definition, in CBPV.EquationalTheory]
one [constructor, in CBPV.Terms]
One [constructor, in CBPV.CBN.CBN]
One [constructor, in CBPV.CBV.CBV]
P
pair [constructor, in CBPV.Syntax]Pair [constructor, in CBPV.CBN.CBN]
Pair [constructor, in CBPV.CBV.CBV]
ParallelReduction [record, in CBPV.Confluence]
parstep [projection, in CBPV.Confluence]
parstepc [inductive, in CBPV.Confluence]
parstepcApp [constructor, in CBPV.Confluence]
parstepcAppBeta [constructor, in CBPV.Confluence]
parstepcCaseP [constructor, in CBPV.Confluence]
parstepcCasePBeta [constructor, in CBPV.Confluence]
parstepcCaseS [constructor, in CBPV.Confluence]
parstepcCaseSBeta [constructor, in CBPV.Confluence]
parstepcCaseZ [constructor, in CBPV.Confluence]
parstepcCu [constructor, in CBPV.Confluence]
parstepcForce [constructor, in CBPV.Confluence]
parstepcForceBeta [constructor, in CBPV.Confluence]
parstepcLambda [constructor, in CBPV.Confluence]
parstepcLetin [constructor, in CBPV.Confluence]
parstepcLetinBeta [constructor, in CBPV.Confluence]
parstepcProj [constructor, in CBPV.Confluence]
parstepcProjBeta [constructor, in CBPV.Confluence]
parstepcRet [constructor, in CBPV.Confluence]
parstepcTuple [constructor, in CBPV.Confluence]
parstepc_subst [definition, in CBPV.Confluence]
parstepc_renaming [definition, in CBPV.Confluence]
parstepc_refl [lemma, in CBPV.Confluence]
parstepc_ind_2 [definition, in CBPV.Confluence]
parstepv [inductive, in CBPV.Confluence]
parstepvInj [constructor, in CBPV.Confluence]
parstepvPair [constructor, in CBPV.Confluence]
parstepvThunk [constructor, in CBPV.Confluence]
parstepvU [constructor, in CBPV.Confluence]
parstepvVar [constructor, in CBPV.Confluence]
parstepv_subst [definition, in CBPV.Confluence]
parstepv_renaming [definition, in CBPV.Confluence]
parstepv_refl [lemma, in CBPV.Confluence]
parstepv_ind_2 [definition, in CBPV.Confluence]
parstep_star_sstep [lemma, in CBPV.Confluence]
parstep_refl [lemma, in CBPV.Confluence]
parstep_comp [instance, in CBPV.Confluence]
parstep_value [instance, in CBPV.Confluence]
pext [axiom, in CBPV.axioms]
Pi [constructor, in CBPV.Syntax]
pi [lemma, in CBPV.axioms]
Pi [constructor, in CBPV.Terms]
plugcctx [definition, in CBPV.ProgramContexts]
plugvctx [definition, in CBPV.ProgramContexts]
plug_fill_cctx_comp [definition, in CBPV.ProgramContexts]
plug_fill_cctx_value [definition, in CBPV.ProgramContexts]
plug_fill_vctx_comp [definition, in CBPV.ProgramContexts]
plug_fill_vctx_value [definition, in CBPV.ProgramContexts]
Plus [constructor, in CBPV.CBN.CBN]
Plus [constructor, in CBPV.CBV.CBV]
plus [inductive, in CBPV.AbstractReductionSystems]
plusSingle [constructor, in CBPV.AbstractReductionSystems]
plusStep [constructor, in CBPV.AbstractReductionSystems]
plus_sstep_value_preserves [lemma, in CBPV.CBV.strongStory]
plus_proper_sstep_letinL' [instance, in CBPV.CBV.strongStory]
plus_transitive [instance, in CBPV.AbstractReductionSystems]
plus_expansive [instance, in CBPV.AbstractReductionSystems]
plus_fixpoint [lemma, in CBPV.AbstractReductionSystems]
plus_idem [lemma, in CBPV.AbstractReductionSystems]
plus_mono [lemma, in CBPV.AbstractReductionSystems]
plus_star_step [lemma, in CBPV.AbstractReductionSystems]
plus_destruct [lemma, in CBPV.AbstractReductionSystems]
plus_star [lemma, in CBPV.AbstractReductionSystems]
plus_exp [lemma, in CBPV.AbstractReductionSystems]
plus_trans [lemma, in CBPV.AbstractReductionSystems]
plus_sstep_preserves [instance, in CBPV.StrongReduction]
plus_proper_sstep_caseP2 [instance, in CBPV.StrongReduction]
plus_proper_sstep_caseP1 [instance, in CBPV.StrongReduction]
plus_proper_sstep_caseS3 [instance, in CBPV.StrongReduction]
plus_proper_sstep_caseS2 [instance, in CBPV.StrongReduction]
plus_proper_sstep_caseS1 [instance, in CBPV.StrongReduction]
plus_proper_sstep_proj [instance, in CBPV.StrongReduction]
plus_proper_sstep_letinR [instance, in CBPV.StrongReduction]
plus_proper_sstep_letinL [instance, in CBPV.StrongReduction]
plus_proper_sstep_ret [instance, in CBPV.StrongReduction]
plus_proper_sstep_tupleR [instance, in CBPV.StrongReduction]
plus_proper_sstep_tupleL [instance, in CBPV.StrongReduction]
plus_proper_sstep_appR [instance, in CBPV.StrongReduction]
plus_proper_sstep_appL [instance, in CBPV.StrongReduction]
plus_proper_sstep_lambda [instance, in CBPV.StrongReduction]
plus_proper_sstep_force [instance, in CBPV.StrongReduction]
plus_proper_sstep_thunk [instance, in CBPV.StrongReduction]
plus_proper_sstep_inj [instance, in CBPV.StrongReduction]
plus_proper_sstep_pairR [instance, in CBPV.StrongReduction]
plus_proper_sstep_pairL [instance, in CBPV.StrongReduction]
preservation [lemma, in CBPV.SyntacticTyping]
preservation_steps [lemma, in CBPV.SyntacticTyping]
primitive_preservation [lemma, in CBPV.SyntacticTyping]
primitive_step_subst_value [definition, in CBPV.StrongReduction]
primitive_step_subst [definition, in CBPV.StrongReduction]
product_t_algebra [definition, in CBPV.DenotationalSemantics]
ProgramContexts [library]
progress [lemma, in CBPV.SyntacticTyping]
proj [constructor, in CBPV.Syntax]
Proj [constructor, in CBPV.CBN.CBN]
Properties [section, in CBPV.AbstractReductionSystems]
Properties.X [variable, in CBPV.AbstractReductionSystems]
proper_Step_Case3 [instance, in CBPV.CBN.strongStory]
proper_Step_Case2 [instance, in CBPV.CBN.strongStory]
proper_Step_Case [instance, in CBPV.CBN.strongStory]
proper_Step_Inj [instance, in CBPV.CBN.strongStory]
proper_Step_Proj [instance, in CBPV.CBN.strongStory]
proper_Step_Lam [instance, in CBPV.CBN.strongStory]
proper_Step_App2 [instance, in CBPV.CBN.strongStory]
proper_Step_App [instance, in CBPV.CBN.strongStory]
proper_Step_Pair2 [instance, in CBPV.CBN.strongStory]
proper_Step_Pair [instance, in CBPV.CBN.strongStory]
proper_Step_Case [instance, in CBPV.CBN.weakStory]
proper_Step_Proj [instance, in CBPV.CBN.weakStory]
proper_Step_App [instance, in CBPV.CBN.weakStory]
proper_eagerlet_plus_sstep_L [lemma, in CBPV.Eagerlet]
proper_eagerlet_sstep_L [lemma, in CBPV.Eagerlet]
proper_eagerlet_star_sstep [lemma, in CBPV.Eagerlet]
proper_eagerlet_star_sstep_L [instance, in CBPV.Eagerlet]
proper_eagerlet_sstep_L_star [instance, in CBPV.Eagerlet]
proper_eagerlet_plus_sstep_R [instance, in CBPV.Eagerlet]
proper_eagerlet_star_ssstep_R [instance, in CBPV.Eagerlet]
proper_eagerlet_sstep_R [instance, in CBPV.Eagerlet]
proper_eagerlet_plus_step_L [instance, in CBPV.Eagerlet]
proper_eagerlet_star_step_L [instance, in CBPV.Eagerlet]
proper_proj [instance, in CBPV.Semantics]
proper_app [instance, in CBPV.Semantics]
proper_letin [instance, in CBPV.Semantics]
proper_Step_Pair [instance, in CBPV.CBV.strongStory]
proper_Step_Lam [instance, in CBPV.CBV.strongStory]
proper_Step_Inj [instance, in CBPV.CBV.strongStory]
proper_Step_Val [instance, in CBPV.CBV.strongStory]
proper_Step_CaseP [instance, in CBPV.CBV.strongStory]
proper_Step_Case [instance, in CBPV.CBV.strongStory]
proper_Step_App [instance, in CBPV.CBV.strongStory]
proper_Step_CaseP [instance, in CBPV.CBV.weakStory]
proper_Step_Case [instance, in CBPV.CBV.weakStory]
proper_Step_App [instance, in CBPV.CBV.weakStory]
proper_subst_comp [lemma, in CBPV.StrongReduction]
proper_sstep_caseP2 [instance, in CBPV.StrongReduction]
proper_sstep_caseP1 [instance, in CBPV.StrongReduction]
proper_sstep_caseS3 [instance, in CBPV.StrongReduction]
proper_sstep_caseS2 [instance, in CBPV.StrongReduction]
proper_sstep_caseS1 [instance, in CBPV.StrongReduction]
proper_sstep_caseZ [instance, in CBPV.StrongReduction]
proper_sstep_proj [instance, in CBPV.StrongReduction]
proper_sstep_letinR [instance, in CBPV.StrongReduction]
proper_sstep_letinL [instance, in CBPV.StrongReduction]
proper_sstep_ret [instance, in CBPV.StrongReduction]
proper_sstep_tupleR [instance, in CBPV.StrongReduction]
proper_sstep_tupleL [instance, in CBPV.StrongReduction]
proper_sstep_appR [instance, in CBPV.StrongReduction]
proper_sstep_appL [instance, in CBPV.StrongReduction]
proper_sstep_lambda [instance, in CBPV.StrongReduction]
proper_sstep_force [instance, in CBPV.StrongReduction]
proper_sstep_thunk [instance, in CBPV.StrongReduction]
proper_sstep_inj [instance, in CBPV.StrongReduction]
proper_sstep_pairR [instance, in CBPV.StrongReduction]
proper_sstep_pairL [instance, in CBPV.StrongReduction]
pstep [inductive, in CBPV.Semantics]
pstepApp [constructor, in CBPV.Semantics]
pstepCaseP [constructor, in CBPV.Semantics]
pstepCaseS [constructor, in CBPV.Semantics]
pstepForce [constructor, in CBPV.Semantics]
pstepLetin [constructor, in CBPV.Semantics]
pstepProj [constructor, in CBPV.Semantics]
pstep_subst [lemma, in CBPV.Semantics]
pstep_value_preserves_ren [lemma, in CBPV.CBV.strongStory]
pstep_subrel [instance, in CBPV.StrongReduction]
pstep_anti_renaming [lemma, in CBPV.StrongReduction]
R
RC [definition, in CBPV.DenotationalSemantics]refines [inductive, in CBPV.CBN.CBN_CBPV]
refines_steps [lemma, in CBPV.CBN.strongStory]
refines_step [lemma, in CBPV.CBN.strongStory]
refines_to_eval [lemma, in CBPV.CBN.strongStory]
refines_steps [lemma, in CBPV.CBN.weakStory]
refines_step [lemma, in CBPV.CBN.weakStory]
refines_beta [lemma, in CBPV.CBN.weakStory]
refines_functional [lemma, in CBPV.CBN.CBN_CBPV]
refines_subst [lemma, in CBPV.CBN.CBN_CBPV]
refines_ren [lemma, in CBPV.CBN.CBN_CBPV]
refines_help [lemma, in CBPV.CBN.CBN_CBPV]
refines_FT [constructor, in CBPV.CBN.CBN_CBPV]
refines_CaseS2 [constructor, in CBPV.CBN.CBN_CBPV]
refines_CaseS [constructor, in CBPV.CBN.CBN_CBPV]
refines_Inj [constructor, in CBPV.CBN.CBN_CBPV]
refines_Proj [constructor, in CBPV.CBN.CBN_CBPV]
refines_Pair [constructor, in CBPV.CBN.CBN_CBPV]
refines_App [constructor, in CBPV.CBN.CBN_CBPV]
refines_Lam [constructor, in CBPV.CBN.CBN_CBPV]
refines_One [constructor, in CBPV.CBN.CBN_CBPV]
refines_var [constructor, in CBPV.CBN.CBN_CBPV]
refl_steps [lemma, in CBPV.DenotationalSemantics]
refl_equiv [lemma, in CBPV.AbstractReductionSystems]
refl_star [lemma, in CBPV.AbstractReductionSystems]
ren [definition, in CBPV.fintype]
renComp_comp [lemma, in CBPV.Syntax]
renComp_value [lemma, in CBPV.Syntax]
renComp_exp [lemma, in CBPV.CBN.CBN]
renComp_Exp [lemma, in CBPV.CBV.CBV]
renComp_Value [lemma, in CBPV.CBV.CBV]
renComp'_comp [lemma, in CBPV.Syntax]
renComp'_value [lemma, in CBPV.Syntax]
renComp'_exp [lemma, in CBPV.CBN.CBN]
renComp'_Exp [lemma, in CBPV.CBV.CBV]
renComp'_Value [lemma, in CBPV.CBV.CBV]
renRen_comp [lemma, in CBPV.Syntax]
renRen_value [lemma, in CBPV.Syntax]
renRen_exp [lemma, in CBPV.CBN.CBN]
renRen_Exp [lemma, in CBPV.CBV.CBV]
renRen_Value [lemma, in CBPV.CBV.CBV]
renRen'_comp [lemma, in CBPV.Syntax]
renRen'_value [lemma, in CBPV.Syntax]
renRen'_exp [lemma, in CBPV.CBN.CBN]
renRen'_Exp [lemma, in CBPV.CBV.CBV]
renRen'_Value [lemma, in CBPV.CBV.CBV]
Ren_comp [instance, in CBPV.Syntax]
Ren_value [instance, in CBPV.Syntax]
ren_comp [definition, in CBPV.Syntax]
ren_value [definition, in CBPV.Syntax]
ren_up_inj [lemma, in CBPV.CBN.CBN_CBPV]
ren_inj [lemma, in CBPV.CBN.CBN_CBPV]
ren_comp_eval [lemma, in CBPV.CBN.CBN_CBPV]
ren_up [abbreviation, in CBPV.CBN.CBN_CBPV]
Ren_exp [instance, in CBPV.CBN.CBN]
ren_exp [definition, in CBPV.CBN.CBN]
Ren_Exp [instance, in CBPV.CBV.CBV]
Ren_Value [instance, in CBPV.CBV.CBV]
ren_Exp [definition, in CBPV.CBV.CBV]
ren_Value [definition, in CBPV.CBV.CBV]
ren_lift [lemma, in CBPV.Confluence]
ren_value_proper [instance, in CBPV.StrongReduction]
ren_comp_proper [instance, in CBPV.StrongReduction]
ren1 [projection, in CBPV.fintype]
Ren1 [record, in CBPV.fintype]
ren1 [constructor, in CBPV.fintype]
Ren1 [inductive, in CBPV.fintype]
ren2 [projection, in CBPV.fintype]
Ren2 [record, in CBPV.fintype]
ren2 [constructor, in CBPV.fintype]
Ren2 [inductive, in CBPV.fintype]
ren₂_lift [lemma, in CBPV.Confluence]
ret [constructor, in CBPV.Syntax]
ret_plus_inv [lemma, in CBPV.CBV.strongStory]
ret_star_inv [lemma, in CBPV.StrongReduction]
rho [definition, in CBPV.Confluence]
rhoᵥ [definition, in CBPV.Confluence]
rinstInst_comp [lemma, in CBPV.Syntax]
rinstInst_value [lemma, in CBPV.Syntax]
rinstInst_up_value_value [definition, in CBPV.Syntax]
rinstInst_exp [lemma, in CBPV.CBN.CBN]
rinstInst_up_exp_exp [definition, in CBPV.CBN.CBN]
rinstInst_Exp [lemma, in CBPV.CBV.CBV]
rinstInst_Value [lemma, in CBPV.CBV.CBV]
rinstInst_up_Value_Value [definition, in CBPV.CBV.CBV]
rinst_inst_comp [definition, in CBPV.Syntax]
rinst_inst_value [definition, in CBPV.Syntax]
rinst_inst_exp [definition, in CBPV.CBN.CBN]
rinst_inst_Exp [definition, in CBPV.CBV.CBV]
rinst_inst_Value [definition, in CBPV.CBV.CBV]
RV [definition, in CBPV.DenotationalSemantics]
S
sandwich_confluent [lemma, in CBPV.TMT]sandwich_equiv [lemma, in CBPV.TMT]
scons [definition, in CBPV.fintype]
scons_comp [lemma, in CBPV.fintype]
scons_eta_id [lemma, in CBPV.fintype]
scons_eta [lemma, in CBPV.fintype]
Semantics [library]
SemanticSoundness [lemma, in CBPV.SemanticTyping]
SemanticSoundness [lemma, in CBPV.StrongNormalisation]
SemanticTyping [library]
semi_confluent [definition, in CBPV.AbstractReductionSystems]
shift [definition, in CBPV.fintype]
Sigma [constructor, in CBPV.Syntax]
Sigma [constructor, in CBPV.Terms]
singleton_t_algebra [definition, in CBPV.DenotationalSemantics]
SN [inductive, in CBPV.AbstractReductionSystems]
sn [definition, in CBPV.StrongReduction]
SNC [constructor, in CBPV.AbstractReductionSystems]
snv [definition, in CBPV.StrongReduction]
SN_CBN [lemma, in CBPV.CBN.strongStory]
SN_CBV [lemma, in CBPV.CBV.strongStory]
SN_CBVᵥ [lemma, in CBPV.CBV.strongStory]
SN_finite_steps [lemma, in CBPV.AbstractReductionSystems]
SN_morphism [lemma, in CBPV.AbstractReductionSystems]
SN_plus [lemma, in CBPV.AbstractReductionSystems]
SN_unfold [lemma, in CBPV.AbstractReductionSystems]
SN_ext [lemma, in CBPV.AbstractReductionSystems]
soundness [lemma, in CBPV.DenotationalSemantics]
sstep [inductive, in CBPV.StrongReduction]
sstepAppL [constructor, in CBPV.StrongReduction]
sstepAppR [constructor, in CBPV.StrongReduction]
sstepCasePC [constructor, in CBPV.StrongReduction]
sstepCasePV [constructor, in CBPV.StrongReduction]
sstepCaseSL [constructor, in CBPV.StrongReduction]
sstepCaseSR [constructor, in CBPV.StrongReduction]
sstepCaseSV [constructor, in CBPV.StrongReduction]
sstepCaseZ [constructor, in CBPV.StrongReduction]
sstepForce [constructor, in CBPV.StrongReduction]
sstepLambda [constructor, in CBPV.StrongReduction]
sstepLetinL [constructor, in CBPV.StrongReduction]
sstepLetinR [constructor, in CBPV.StrongReduction]
sstepPrimitive [constructor, in CBPV.StrongReduction]
sstepProj [constructor, in CBPV.StrongReduction]
sstepRet [constructor, in CBPV.StrongReduction]
ssteps_preservation [lemma, in CBPV.StrongReduction]
sstepTupleL [constructor, in CBPV.StrongReduction]
sstepTupleR [constructor, in CBPV.StrongReduction]
sstepValueInj [constructor, in CBPV.StrongReduction]
sstepValuePairL [constructor, in CBPV.StrongReduction]
sstepValuePairR [constructor, in CBPV.StrongReduction]
sstepValueThunk [constructor, in CBPV.StrongReduction]
sstep_value_preserves_ren [lemma, in CBPV.CBV.strongStory]
sstep_value_confluent [lemma, in CBPV.Confluence]
sstep_confluent [lemma, in CBPV.Confluence]
sstep_value_parstepv [definition, in CBPV.Confluence]
sstep_parstepc [definition, in CBPV.Confluence]
sstep_value_anti_renaming [definition, in CBPV.StrongReduction]
sstep_anti_renaming [definition, in CBPV.StrongReduction]
sstep_preservation [lemma, in CBPV.StrongReduction]
sstep_progress [lemma, in CBPV.StrongReduction]
sstep_strong_step_value [lemma, in CBPV.StrongReduction]
sstep_strong_step [lemma, in CBPV.StrongReduction]
sstep_value_lemma [definition, in CBPV.StrongReduction]
sstep_lemma [definition, in CBPV.StrongReduction]
sstep_value_congruence_value [definition, in CBPV.StrongReduction]
sstep_value_congruence [definition, in CBPV.StrongReduction]
sstep_congruence_value [definition, in CBPV.StrongReduction]
sstep_congruence [definition, in CBPV.StrongReduction]
sstep_ind_2 [definition, in CBPV.StrongReduction]
sstep_value_ind_2 [definition, in CBPV.StrongReduction]
sstep_value [inductive, in CBPV.StrongReduction]
star [inductive, in CBPV.AbstractReductionSystems]
starL [inductive, in CBPV.AbstractReductionSystems]
starRefl [constructor, in CBPV.AbstractReductionSystems]
starReflL [constructor, in CBPV.AbstractReductionSystems]
starStep [constructor, in CBPV.AbstractReductionSystems]
starStepL [constructor, in CBPV.AbstractReductionSystems]
starstep_functional_nf [lemma, in CBPV.Semantics]
star_expansive [instance, in CBPV.AbstractReductionSystems]
star_preorder [instance, in CBPV.AbstractReductionSystems]
star_starL [lemma, in CBPV.AbstractReductionSystems]
star_absorbtion [lemma, in CBPV.AbstractReductionSystems]
star_idem [lemma, in CBPV.AbstractReductionSystems]
star_closure [lemma, in CBPV.AbstractReductionSystems]
star_mono [lemma, in CBPV.AbstractReductionSystems]
star_exp [lemma, in CBPV.AbstractReductionSystems]
star_trans [lemma, in CBPV.AbstractReductionSystems]
star_sstep_preserves_value [instance, in CBPV.StrongReduction]
star_sstep_preserves [instance, in CBPV.StrongReduction]
Step [inductive, in CBPV.CBN.strongStory]
Step [inductive, in CBPV.CBN.weakStory]
step [inductive, in CBPV.Semantics]
Step [inductive, in CBPV.CBV.strongStory]
Step [inductive, in CBPV.CBV.weakStory]
stepApp [constructor, in CBPV.Semantics]
StepAppLam [constructor, in CBPV.CBN.strongStory]
StepAppLam [constructor, in CBPV.CBN.weakStory]
StepAppLam [constructor, in CBPV.CBV.strongStory]
StepAppLam [constructor, in CBPV.CBV.weakStory]
StepApp1 [constructor, in CBPV.CBN.strongStory]
StepApp1 [constructor, in CBPV.CBN.weakStory]
StepApp1 [constructor, in CBPV.CBV.strongStory]
StepApp1 [constructor, in CBPV.CBV.weakStory]
StepApp2 [constructor, in CBPV.CBN.strongStory]
StepApp2 [constructor, in CBPV.CBV.strongStory]
StepApp2 [constructor, in CBPV.CBV.weakStory]
StepCaseP [constructor, in CBPV.CBV.strongStory]
StepCaseP [constructor, in CBPV.CBV.weakStory]
StepCaseP1 [constructor, in CBPV.CBV.strongStory]
StepCaseP1 [constructor, in CBPV.CBV.weakStory]
StepCaseP2 [constructor, in CBPV.CBV.strongStory]
StepCaseS [constructor, in CBPV.CBN.strongStory]
StepCaseS [constructor, in CBPV.CBN.weakStory]
StepCaseS [constructor, in CBPV.CBV.strongStory]
StepCaseS [constructor, in CBPV.CBV.weakStory]
StepCaseS1 [constructor, in CBPV.CBN.strongStory]
StepCaseS1 [constructor, in CBPV.CBN.weakStory]
StepCaseS1 [constructor, in CBPV.CBV.strongStory]
StepCaseS1 [constructor, in CBPV.CBV.weakStory]
StepCaseS2 [constructor, in CBPV.CBN.strongStory]
StepCaseS2 [constructor, in CBPV.CBV.strongStory]
StepCaseS3 [constructor, in CBPV.CBN.strongStory]
StepCaseS3 [constructor, in CBPV.CBV.strongStory]
StepInj [constructor, in CBPV.CBN.strongStory]
StepInj [constructor, in CBPV.CBV.strongStory]
StepLam [constructor, in CBPV.CBN.strongStory]
StepLam [constructor, in CBPV.CBV.strongStory]
stepLetin [constructor, in CBPV.Semantics]
StepPair1 [constructor, in CBPV.CBN.strongStory]
StepPair1 [constructor, in CBPV.CBV.strongStory]
StepPair2 [constructor, in CBPV.CBN.strongStory]
StepPair2 [constructor, in CBPV.CBV.strongStory]
stepPrimitive [constructor, in CBPV.Semantics]
StepProj [constructor, in CBPV.CBN.strongStory]
StepProj [constructor, in CBPV.CBN.weakStory]
stepProj [constructor, in CBPV.Semantics]
StepProjPair [constructor, in CBPV.CBN.strongStory]
StepProjPair [constructor, in CBPV.CBN.weakStory]
Steps_backwards [lemma, in CBPV.CBN.strongStory]
Steps_preserved [lemma, in CBPV.CBN.strongStory]
Steps_preserved [lemma, in CBPV.CBN.weakStory]
steps_bigstep [lemma, in CBPV.Semantics]
steps_nf_eval [lemma, in CBPV.Semantics]
StepVal [inductive, in CBPV.CBV.strongStory]
StepValue [constructor, in CBPV.CBV.strongStory]
StepVal_preserved [definition, in CBPV.CBV.strongStory]
stepv_thunk_inv [lemma, in CBPV.StrongReduction]
stepv_inj_inv [lemma, in CBPV.StrongReduction]
stepv_pair_inv [lemma, in CBPV.StrongReduction]
stepv_u_inv [lemma, in CBPV.StrongReduction]
stepv_var_inv [lemma, in CBPV.StrongReduction]
Step_inj_inv [lemma, in CBPV.CBN.strongStory]
Step_preserved [lemma, in CBPV.CBN.strongStory]
Step_preserved_refines [lemma, in CBPV.CBN.weakStory]
Step_preserved [lemma, in CBPV.CBN.weakStory]
step_equiv [lemma, in CBPV.Semantics]
step_functional [lemma, in CBPV.Semantics]
Step_preserved [definition, in CBPV.CBV.strongStory]
Step_preserved [lemma, in CBPV.CBV.weakStory]
step_star_plus [lemma, in CBPV.AbstractReductionSystems]
step_ren_comp_inv [lemma, in CBPV.StrongReduction]
step_caseP_inv [lemma, in CBPV.StrongReduction]
step_caseS_inv [lemma, in CBPV.StrongReduction]
step_caseZ_inv [lemma, in CBPV.StrongReduction]
step_proj_inv [lemma, in CBPV.StrongReduction]
step_letin_inv [lemma, in CBPV.StrongReduction]
step_ret_inv [lemma, in CBPV.StrongReduction]
step_tuple_inv [lemma, in CBPV.StrongReduction]
step_app_inv [lemma, in CBPV.StrongReduction]
step_lambda_inv [lemma, in CBPV.StrongReduction]
step_force_inv [lemma, in CBPV.StrongReduction]
step_cu_inv [lemma, in CBPV.StrongReduction]
step_strong [lemma, in CBPV.StrongReduction]
StrongNormalisation [section, in CBPV.AbstractReductionSystems]
StrongNormalisation [library]
StrongNormalisation.A [variable, in CBPV.AbstractReductionSystems]
StrongNormalisation.R [variable, in CBPV.AbstractReductionSystems]
StrongNormalisation.S [variable, in CBPV.AbstractReductionSystems]
StrongNormalisation.X [variable, in CBPV.AbstractReductionSystems]
StrongReduction [library]
strongStory [library]
strongStory [library]
strong_normalisation [lemma, in CBPV.StrongNormalisation]
strong_normalisation_cbv [lemma, in CBPV.Termination]
strong_normalisation_cbvᵥ [lemma, in CBPV.Termination]
strong_normalisation_cbn [lemma, in CBPV.Termination]
strong_normalisation_cbpvᵥ [lemma, in CBPV.Termination]
strong_normalisation_cbpv [lemma, in CBPV.Termination]
strong_step_value_anti_renaming [lemma, in CBPV.StrongReduction]
strong_step_anti_renaming [lemma, in CBPV.StrongReduction]
strong_step_value_subst [lemma, in CBPV.StrongReduction]
strong_step_subst [lemma, in CBPV.StrongReduction]
strong_step_value_preservation [lemma, in CBPV.StrongReduction]
strong_step_preservation [lemma, in CBPV.StrongReduction]
strong_step_progress [lemma, in CBPV.StrongReduction]
strong_step_value_congruence_value [lemma, in CBPV.StrongReduction]
strong_step_value_congruence [lemma, in CBPV.StrongReduction]
strong_step_congruence_value [lemma, in CBPV.StrongReduction]
strong_step_congruence [lemma, in CBPV.StrongReduction]
strong_reduce_value [constructor, in CBPV.StrongReduction]
strong_step_value [inductive, in CBPV.StrongReduction]
strong_reduce [constructor, in CBPV.StrongReduction]
strong_step [inductive, in CBPV.StrongReduction]
sub [definition, in CBPV.EquationalTheory]
subrel_C_E [instance, in CBPV.LogicalEquivalence]
subrel_star_equiv [instance, in CBPV.AbstractReductionSystems]
subrel_plus_mono [instance, in CBPV.AbstractReductionSystems]
subrel_star_mono [instance, in CBPV.AbstractReductionSystems]
subrel_star [instance, in CBPV.AbstractReductionSystems]
subrel_step_sstep [instance, in CBPV.StrongReduction]
Subst_comp [instance, in CBPV.Syntax]
Subst_value [instance, in CBPV.Syntax]
subst_comp [definition, in CBPV.Syntax]
subst_value [definition, in CBPV.Syntax]
subst_pres [lemma, in CBPV.CBN.strongStory]
subst_pointwise [lemma, in CBPV.CBN.strongStory]
Subst_exp [instance, in CBPV.CBN.CBN]
subst_exp [definition, in CBPV.CBN.CBN]
Subst_Exp [instance, in CBPV.CBV.CBV]
Subst_Value [instance, in CBPV.CBV.CBV]
subst_Exp [definition, in CBPV.CBV.CBV]
subst_Value [definition, in CBPV.CBV.CBV]
subst1 [projection, in CBPV.fintype]
Subst1 [record, in CBPV.fintype]
subst1 [constructor, in CBPV.fintype]
Subst1 [inductive, in CBPV.fintype]
subst2 [projection, in CBPV.fintype]
Subst2 [record, in CBPV.fintype]
subst2 [constructor, in CBPV.fintype]
Subst2 [inductive, in CBPV.fintype]
sub₂ [definition, in CBPV.EquationalTheory]
swap [definition, in CBPV.EquationalTheory]
sym [inductive, in CBPV.AbstractReductionSystems]
symId [constructor, in CBPV.AbstractReductionSystems]
symInv [constructor, in CBPV.AbstractReductionSystems]
sym_Symmetric [instance, in CBPV.AbstractReductionSystems]
sym_symmetric [lemma, in CBPV.AbstractReductionSystems]
SyntacticTyping [library]
Syntax [library]
T
T [projection, in CBPV.DenotationalSemantics]Takahashi [section, in CBPV.TMT]
takahashi [lemma, in CBPV.Confluence]
Takahashi.R [variable, in CBPV.TMT]
Takahashi.rho [variable, in CBPV.TMT]
Takahashi.tak [variable, in CBPV.TMT]
Takahashi.X [variable, in CBPV.TMT]
_ >* _ [notation, in CBPV.TMT]
_ > _ [notation, in CBPV.TMT]
tak_cofinal [lemma, in CBPV.TMT]
tak_mono_n [lemma, in CBPV.TMT]
tak_mono [lemma, in CBPV.TMT]
tak_sound [lemma, in CBPV.TMT]
tak_diamond [lemma, in CBPV.TMT]
tak_fun [definition, in CBPV.TMT]
TAlgebra [record, in CBPV.DenotationalSemantics]
TAlgebra [section, in CBPV.DenotationalSemantics]
TAlgebra.T [variable, in CBPV.DenotationalSemantics]
terminal_step [lemma, in CBPV.CBN.strongStory]
Termination [library]
Terms [library]
thunk [constructor, in CBPV.Syntax]
thunk_star_inv [lemma, in CBPV.StrongReduction]
TMT [lemma, in CBPV.TMT]
TMT [section, in CBPV.TMT]
TMT [library]
TMT.H1 [variable, in CBPV.TMT]
TMT.H2 [variable, in CBPV.TMT]
TMT.R [variable, in CBPV.TMT]
TMT.S [variable, in CBPV.TMT]
TMT.X [variable, in CBPV.TMT]
to_valtype [definition, in CBPV.Terms]
trans [inductive, in CBPV.CBN.CBN_CBPV]
trans_beta [lemma, in CBPV.CBN.weakStory]
trans_subst_exp [lemma, in CBPV.CBV.CBV_CBPV]
trans_subst_val [lemma, in CBPV.CBV.CBV_CBPV]
trans_subst_val' [lemma, in CBPV.CBV.CBV_CBPV]
trans_ren_exp [lemma, in CBPV.CBV.CBV_CBPV]
trans_ren_val [lemma, in CBPV.CBV.CBV_CBPV]
trans_ren_val' [lemma, in CBPV.CBV.CBV_CBPV]
trans_inj [lemma, in CBPV.CBN.CBN_CBPV]
trans_refines [lemma, in CBPV.CBN.CBN_CBPV]
trans_eval [lemma, in CBPV.CBN.CBN_CBPV]
trans_subst [lemma, in CBPV.CBN.CBN_CBPV]
trans_ren [lemma, in CBPV.CBN.CBN_CBPV]
trans_preserves [lemma, in CBPV.CBN.CBN_CBPV]
trans_FT [constructor, in CBPV.CBN.CBN_CBPV]
trans_CaseS [constructor, in CBPV.CBN.CBN_CBPV]
trans_Inj [constructor, in CBPV.CBN.CBN_CBPV]
trans_Proj [constructor, in CBPV.CBN.CBN_CBPV]
trans_Pair [constructor, in CBPV.CBN.CBN_CBPV]
trans_App [constructor, in CBPV.CBN.CBN_CBPV]
trans_Lam [constructor, in CBPV.CBN.CBN_CBPV]
trans_One [constructor, in CBPV.CBN.CBN_CBPV]
trans_var [constructor, in CBPV.CBN.CBN_CBPV]
tt [definition, in CBPV.CBN.DenotationalSemantics]
tt [definition, in CBPV.CBV.DenotationalSemantics]
tuple [constructor, in CBPV.Syntax]
type [inductive, in CBPV.CBN.CBN]
type [inductive, in CBPV.CBV.CBV]
typeApp [constructor, in CBPV.CBV.CBV_CBPV]
typeApp [constructor, in CBPV.SyntacticTyping]
typeCaseP [constructor, in CBPV.CBV.CBV_CBPV]
typeCaseP [constructor, in CBPV.SyntacticTyping]
typeCaseS [constructor, in CBPV.CBV.CBV_CBPV]
typeCaseS [constructor, in CBPV.SyntacticTyping]
typeCaseZ [constructor, in CBPV.SyntacticTyping]
typeCone [constructor, in CBPV.SyntacticTyping]
typeForce [constructor, in CBPV.SyntacticTyping]
typeInjL [constructor, in CBPV.CBV.CBV_CBPV]
typeLam [constructor, in CBPV.CBV.CBV_CBPV]
typeLambda [constructor, in CBPV.SyntacticTyping]
typeLetin [constructor, in CBPV.SyntacticTyping]
typeOne [constructor, in CBPV.CBV.CBV_CBPV]
typePair [constructor, in CBPV.CBV.CBV_CBPV]
typePair [constructor, in CBPV.SyntacticTyping]
typepres_beta [lemma, in CBPV.SyntacticTyping]
typeProj [constructor, in CBPV.SyntacticTyping]
typeRet [constructor, in CBPV.SyntacticTyping]
typeSum [constructor, in CBPV.SyntacticTyping]
typeThunk [constructor, in CBPV.SyntacticTyping]
typeTuple [constructor, in CBPV.SyntacticTyping]
typeUnit [constructor, in CBPV.SyntacticTyping]
typeVal [constructor, in CBPV.CBV.CBV_CBPV]
typeVar [constructor, in CBPV.SyntacticTyping]
typeVarV [constructor, in CBPV.CBV.CBV_CBPV]
typeVar' [lemma, in CBPV.SyntacticTyping]
typingExp_pres [definition, in CBPV.CBV.CBV_CBPV]
typingExp_pres' [definition, in CBPV.CBV.DenotationalSemantics]
TypingLemmas [section, in CBPV.StrongNormalisation]
TypingLemmas.A [variable, in CBPV.StrongNormalisation]
TypingLemmas.A1 [variable, in CBPV.StrongNormalisation]
TypingLemmas.A2 [variable, in CBPV.StrongNormalisation]
TypingLemmas.B [variable, in CBPV.StrongNormalisation]
TypingLemmas.B1 [variable, in CBPV.StrongNormalisation]
TypingLemmas.B2 [variable, in CBPV.StrongNormalisation]
TypingLemmas.Gamma [variable, in CBPV.StrongNormalisation]
TypingLemmas.n [variable, in CBPV.StrongNormalisation]
typingVal_pres [definition, in CBPV.CBV.CBV_CBPV]
typingVal_pres' [definition, in CBPV.CBV.DenotationalSemantics]
t_algebra2 [projection, in CBPV.DenotationalSemantics]
t_algebra1 [projection, in CBPV.DenotationalSemantics]
U
u [constructor, in CBPV.Syntax]U [constructor, in CBPV.Syntax]
U [constructor, in CBPV.Terms]
Unit [constructor, in CBPV.CBN.CBN]
Unit [constructor, in CBPV.CBV.CBV]
upExtRen_value_value [definition, in CBPV.Syntax]
upExtRen_exp_exp [definition, in CBPV.CBN.CBN]
upExtRen_Value_Value [definition, in CBPV.CBV.CBV]
upExt_value_value [definition, in CBPV.Syntax]
upExt_exp_exp [definition, in CBPV.CBN.CBN]
upExt_Value_Value [definition, in CBPV.CBV.CBV]
upId_value_value [definition, in CBPV.Syntax]
upId_exp_exp [definition, in CBPV.CBN.CBN]
upId_Value_Value [definition, in CBPV.CBV.CBV]
upRen_value_value [definition, in CBPV.Syntax]
upRen_exp_exp [definition, in CBPV.CBN.CBN]
upRen_Value_Value [definition, in CBPV.CBV.CBV]
up_subst_subst_value_value [definition, in CBPV.Syntax]
up_subst_ren_value_value [definition, in CBPV.Syntax]
up_ren_subst_value_value [definition, in CBPV.Syntax]
up_value_value [definition, in CBPV.Syntax]
up_ren_ren [lemma, in CBPV.fintype]
up_ren [definition, in CBPV.fintype]
up_ren [abbreviation, in CBPV.CBV.CBV_CBPV]
up_subst_subst_exp_exp [definition, in CBPV.CBN.CBN]
up_subst_ren_exp_exp [definition, in CBPV.CBN.CBN]
up_ren_subst_exp_exp [definition, in CBPV.CBN.CBN]
up_exp_exp [definition, in CBPV.CBN.CBN]
up_subst_subst_Value_Value [definition, in CBPV.CBV.CBV]
up_subst_ren_Value_Value [definition, in CBPV.CBV.CBV]
up_ren_subst_Value_Value [definition, in CBPV.CBV.CBV]
up_Value_Value [definition, in CBPV.CBV.CBV]
up2_ren [abbreviation, in CBPV.CBV.CBV_CBPV]
V
V [definition, in CBPV.LogicalEquivalence]V [definition, in CBPV.SemanticTyping]
V [definition, in CBPV.StrongNormalisation]
Val [constructor, in CBPV.CBV.CBV]
valtype [inductive, in CBPV.Syntax]
valtype [inductive, in CBPV.Terms]
valtypeif [definition, in CBPV.ProgramContexts]
valtype_ind_2 [definition, in CBPV.Terms]
value [inductive, in CBPV.Syntax]
Value [inductive, in CBPV.CBV.CBV]
Value_ind_2 [definition, in CBPV.CBV.CBV_CBPV]
value_typepres_substitution [definition, in CBPV.SyntacticTyping]
value_typepres_renaming [definition, in CBPV.SyntacticTyping]
value_typing_ind_4 [definition, in CBPV.SyntacticTyping]
value_typing_ind_3 [definition, in CBPV.SyntacticTyping]
value_typing_ind_2 [definition, in CBPV.SyntacticTyping]
value_typing [inductive, in CBPV.SyntacticTyping]
value_exp_ind_2 [definition, in CBPV.CBV.strongStory]
value_ind_2 [definition, in CBPV.Terms]
value_obseq [definition, in CBPV.ObservationalEquivalence]
value_obseq [definition, in CBPV.CBV.DenotationalSemantics]
val_semeq_trans [instance, in CBPV.LogicalEquivalence]
val_semeq_transitive [lemma, in CBPV.LogicalEquivalence]
val_semeq_symm [instance, in CBPV.LogicalEquivalence]
val_semeq_symmetry [lemma, in CBPV.LogicalEquivalence]
val_semeq [definition, in CBPV.LogicalEquivalence]
val_semtype [definition, in CBPV.SemanticTyping]
val_semtype [definition, in CBPV.StrongNormalisation]
val_obseq_cctx_congruence [lemma, in CBPV.ObservationalEquivalence]
val_obseq_vctx_congruence [lemma, in CBPV.ObservationalEquivalence]
Var [record, in CBPV.fintype]
Var [inductive, in CBPV.fintype]
var [definition, in CBPV.Terms]
VarInstance_value [instance, in CBPV.Syntax]
VarInstance_exp [instance, in CBPV.CBN.CBN]
VarInstance_Value [instance, in CBPV.CBV.CBV]
varLRen_value [lemma, in CBPV.Syntax]
varLRen_exp [lemma, in CBPV.CBN.CBN]
varLRen_Value [lemma, in CBPV.CBV.CBV]
varL_value [lemma, in CBPV.Syntax]
varL_exp [lemma, in CBPV.CBN.CBN]
varL_Value [lemma, in CBPV.CBV.CBV]
var_value [constructor, in CBPV.Syntax]
var_zero [definition, in CBPV.fintype]
var_exp [constructor, in CBPV.CBN.CBN]
var_Value [constructor, in CBPV.CBV.CBV]
vctx [inductive, in CBPV.ProgramContexts]
vctxHole [constructor, in CBPV.ProgramContexts]
vctxInj [constructor, in CBPV.ProgramContexts]
vctxPairL [constructor, in CBPV.ProgramContexts]
vctxPairR [constructor, in CBPV.ProgramContexts]
vctxThunk [constructor, in CBPV.ProgramContexts]
vctxTyping [inductive, in CBPV.ProgramContexts]
vctxTypingHole [constructor, in CBPV.ProgramContexts]
vctxTypingInj [constructor, in CBPV.ProgramContexts]
vctxTypingPairL [constructor, in CBPV.ProgramContexts]
vctxTypingPairR [constructor, in CBPV.ProgramContexts]
vctxTypingThunk [constructor, in CBPV.ProgramContexts]
vctx_comp_typing_soundness [definition, in CBPV.ProgramContexts]
vctx_value_typing_soundness [definition, in CBPV.ProgramContexts]
vctx_cctx_plug_typing_soundness [definition, in CBPV.ProgramContexts]
vctx_vctx_plug_typing_soundness [definition, in CBPV.ProgramContexts]
vctx_typing_ind_3 [definition, in CBPV.ProgramContexts]
vctx_typing_ind_2 [definition, in CBPV.ProgramContexts]
vctx_ind_2 [definition, in CBPV.ProgramContexts]
vctxᵥ [inductive, in CBPV.CBV.DenotationalSemantics]
vctxᵥHole [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥInj [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥLambda [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥPairL [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥPairR [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥTyping [inductive, in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingHole [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingInj [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingLambda [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingPairL [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingPairR [constructor, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_vctx_comp [definition, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_vctx_value [definition, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_comp_typing_soundness [definition, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_value_typing_soundness [definition, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_typing_ind_3 [definition, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_typing_ind_2 [definition, in CBPV.CBV.DenotationalSemantics]
vctxᵥ_ind_2 [definition, in CBPV.CBV.DenotationalSemantics]
VC_ren [lemma, in CBPV.StrongNormalisation]
VV [abbreviation, in CBPV.StrongNormalisation]
VV_sn [lemma, in CBPV.StrongNormalisation]
VV_red [lemma, in CBPV.StrongNormalisation]
VV_var [lemma, in CBPV.StrongNormalisation]
VV_ren [lemma, in CBPV.StrongNormalisation]
V_trans [instance, in CBPV.LogicalEquivalence]
V_C_transitive [lemma, in CBPV.LogicalEquivalence]
V_symm [instance, in CBPV.LogicalEquivalence]
V_C_symmetry [lemma, in CBPV.LogicalEquivalence]
V_sn [lemma, in CBPV.StrongNormalisation]
V_sn_to_VV_sn [lemma, in CBPV.StrongNormalisation]
V_red [lemma, in CBPV.StrongNormalisation]
V_red_to_VV_red [lemma, in CBPV.StrongNormalisation]
W
weakStory [library]weakStory [library]
weak_normalisation_cbv [lemma, in CBPV.Termination]
weak_normalisation_cbn [lemma, in CBPV.Termination]
weak_normalisation_cbpv [lemma, in CBPV.Termination]
weak_simulation [lemma, in CBPV.CBV.weakStory]
WN_translates [lemma, in CBPV.CBN.weakStory]
WN_CBV [lemma, in CBPV.CBV.weakStory]
Z
zero [constructor, in CBPV.Syntax]zero [definition, in CBPV.EquationalTheory]
zero [constructor, in CBPV.Terms]
other
[ _ ] (fscope) [notation, in CBPV.fintype]⟨ _ ⟩ (fscope) [notation, in CBPV.fintype]
⇑__value (subst_scope) [notation, in CBPV.Syntax]
_ __value (subst_scope) [notation, in CBPV.Syntax]
↑ (subst_scope) [notation, in CBPV.fintype]
_ .. (subst_scope) [notation, in CBPV.fintype]
_ .: _ (subst_scope) [notation, in CBPV.fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in CBPV.fintype]
_ [ _ ; _ ] (subst_scope) [notation, in CBPV.fintype]
_ [ _ ] (subst_scope) [notation, in CBPV.fintype]
⇑__exp (subst_scope) [notation, in CBPV.CBN.CBN]
_ __exp (subst_scope) [notation, in CBPV.CBN.CBN]
⇑__Value (subst_scope) [notation, in CBPV.CBV.CBV]
_ __Value (subst_scope) [notation, in CBPV.CBV.CBV]
{ _ & _ } (type_scope) [notation, in CBPV.Base]
_ ↪+ _ [notation, in CBPV.CBN.strongStory]
_ ≫ _ [notation, in CBPV.CBN.strongStory]
_ ⊨ _ ∼ _ : _ [notation, in CBPV.LogicalEquivalence]
_ ⊫ _ ∼ _ : _ [notation, in CBPV.LogicalEquivalence]
_ >> _ [notation, in CBPV.fintype]
_ ≫ _ [notation, in CBPV.CBN.weakStory]
_ ⊢v _ : _ [notation, in CBPV.CBV.CBV_CBPV]
_ ⊩v _ : _ [notation, in CBPV.CBV.CBV_CBPV]
_ [[ _ ]] ⊢ _ : _ ; _ [notation, in CBPV.ProgramContexts]
_ [[ _ ]] ⊩ _ : _ ; _ [notation, in CBPV.ProgramContexts]
_ @ _ [notation, in CBPV.DenotationalSemantics]
_ >>= _ [notation, in CBPV.DenotationalSemantics]
_ ⊨ _ : _ [notation, in CBPV.SemanticTyping]
_ ⊫ _ : _ [notation, in CBPV.SemanticTyping]
_ ▷ _ [notation, in CBPV.Semantics]
_ ⇝ _ [notation, in CBPV.Semantics]
_ >+ _ [notation, in CBPV.Semantics]
_ >* _ [notation, in CBPV.Semantics]
_ > _ [notation, in CBPV.Semantics]
_ ≽ _ [notation, in CBPV.Semantics]
_ ⊢ _ : _ [notation, in CBPV.SyntacticTyping]
_ ⊩ _ : _ [notation, in CBPV.SyntacticTyping]
_ ⊨ _ ::: _ [notation, in CBPV.StrongNormalisation]
_ ⊫ _ ::: _ [notation, in CBPV.StrongNormalisation]
_ ≃n _ [notation, in CBPV.CBN.DenotationalSemantics]
_ ≫* _ [notation, in CBPV.CBN.DenotationalSemantics]
_ [[ _ ]] ⊢n _ : _ ; _ [notation, in CBPV.CBN.DenotationalSemantics]
_ ⋙ _ [notation, in CBPV.CBN.CBN_CBPV]
_ ⋘ _ [notation, in CBPV.CBN.CBN_CBPV]
_ ↦n _ [notation, in CBPV.CBN.CBN_CBPV]
_ ⊢n _ : _ [notation, in CBPV.CBN.CBN_CBPV]
_ * _ [notation, in CBPV.Terms]
_ → _ [notation, in CBPV.Terms]
_ ! [notation, in CBPV.Terms]
_ >+ _ [notation, in CBPV.CBV.weakStory]
_ ≃ _ [notation, in CBPV.ObservationalEquivalence]
_ ≈ _ [notation, in CBPV.ObservationalEquivalence]
_ === _ [notation, in CBPV.AbstractReductionSystems]
_ <<= _ [notation, in CBPV.AbstractReductionSystems]
_ >>c _ [notation, in CBPV.Confluence]
_ >>v _ [notation, in CBPV.Confluence]
_ >> _ [notation, in CBPV.Confluence]
_ ≈v _ [notation, in CBPV.CBV.DenotationalSemantics]
_ ≃v _ [notation, in CBPV.CBV.DenotationalSemantics]
_ ≫* _ [notation, in CBPV.CBV.DenotationalSemantics]
_ [[ _ ]] ⊢v _ : _ ; _ [notation, in CBPV.CBV.DenotationalSemantics]
_ [[ _ ]] ⊩v _ : _ ; _ [notation, in CBPV.CBV.DenotationalSemantics]
_ ↪ᵥ* _ [notation, in CBPV.StrongReduction]
_ ↪* _ [notation, in CBPV.StrongReduction]
_ ↪ᵥ _ [notation, in CBPV.StrongReduction]
_ ↪ _ [notation, in CBPV.StrongReduction]
_ ⇒ᵥ _ [notation, in CBPV.StrongReduction]
_ ⇒ _ [notation, in CBPV.StrongReduction]
$$ <- _ ; _ [notation, in CBPV.Eagerlet]
$ <- _ ; _ [notation, in CBPV.Terms]
<{ _ }> [notation, in CBPV.Terms]
•__c [notation, in CBPV.ProgramContexts]
•__v [notation, in CBPV.ProgramContexts]
• [notation, in CBPV.CBN.DenotationalSemantics]
⟨ _ ; _ ⟩ [notation, in CBPV.Terms]
η [abbreviation, in CBPV.DenotationalSemantics]
Notation Index
C
_ , _ (subst_scope) [in CBPV.fintype]T
_ >* _ [in CBPV.TMT]_ > _ [in CBPV.TMT]
other
[ _ ] (fscope) [in CBPV.fintype]⟨ _ ⟩ (fscope) [in CBPV.fintype]
⇑__value (subst_scope) [in CBPV.Syntax]
_ __value (subst_scope) [in CBPV.Syntax]
↑ (subst_scope) [in CBPV.fintype]
_ .. (subst_scope) [in CBPV.fintype]
_ .: _ (subst_scope) [in CBPV.fintype]
_ ⟨ _ ⟩ (subst_scope) [in CBPV.fintype]
_ [ _ ; _ ] (subst_scope) [in CBPV.fintype]
_ [ _ ] (subst_scope) [in CBPV.fintype]
⇑__exp (subst_scope) [in CBPV.CBN.CBN]
_ __exp (subst_scope) [in CBPV.CBN.CBN]
⇑__Value (subst_scope) [in CBPV.CBV.CBV]
_ __Value (subst_scope) [in CBPV.CBV.CBV]
{ _ & _ } (type_scope) [in CBPV.Base]
_ ↪+ _ [in CBPV.CBN.strongStory]
_ ≫ _ [in CBPV.CBN.strongStory]
_ ⊨ _ ∼ _ : _ [in CBPV.LogicalEquivalence]
_ ⊫ _ ∼ _ : _ [in CBPV.LogicalEquivalence]
_ >> _ [in CBPV.fintype]
_ ≫ _ [in CBPV.CBN.weakStory]
_ ⊢v _ : _ [in CBPV.CBV.CBV_CBPV]
_ ⊩v _ : _ [in CBPV.CBV.CBV_CBPV]
_ [[ _ ]] ⊢ _ : _ ; _ [in CBPV.ProgramContexts]
_ [[ _ ]] ⊩ _ : _ ; _ [in CBPV.ProgramContexts]
_ @ _ [in CBPV.DenotationalSemantics]
_ >>= _ [in CBPV.DenotationalSemantics]
_ ⊨ _ : _ [in CBPV.SemanticTyping]
_ ⊫ _ : _ [in CBPV.SemanticTyping]
_ ▷ _ [in CBPV.Semantics]
_ ⇝ _ [in CBPV.Semantics]
_ >+ _ [in CBPV.Semantics]
_ >* _ [in CBPV.Semantics]
_ > _ [in CBPV.Semantics]
_ ≽ _ [in CBPV.Semantics]
_ ⊢ _ : _ [in CBPV.SyntacticTyping]
_ ⊩ _ : _ [in CBPV.SyntacticTyping]
_ ⊨ _ ::: _ [in CBPV.StrongNormalisation]
_ ⊫ _ ::: _ [in CBPV.StrongNormalisation]
_ ≃n _ [in CBPV.CBN.DenotationalSemantics]
_ ≫* _ [in CBPV.CBN.DenotationalSemantics]
_ [[ _ ]] ⊢n _ : _ ; _ [in CBPV.CBN.DenotationalSemantics]
_ ⋙ _ [in CBPV.CBN.CBN_CBPV]
_ ⋘ _ [in CBPV.CBN.CBN_CBPV]
_ ↦n _ [in CBPV.CBN.CBN_CBPV]
_ ⊢n _ : _ [in CBPV.CBN.CBN_CBPV]
_ * _ [in CBPV.Terms]
_ → _ [in CBPV.Terms]
_ ! [in CBPV.Terms]
_ >+ _ [in CBPV.CBV.weakStory]
_ ≃ _ [in CBPV.ObservationalEquivalence]
_ ≈ _ [in CBPV.ObservationalEquivalence]
_ === _ [in CBPV.AbstractReductionSystems]
_ <<= _ [in CBPV.AbstractReductionSystems]
_ >>c _ [in CBPV.Confluence]
_ >>v _ [in CBPV.Confluence]
_ >> _ [in CBPV.Confluence]
_ ≈v _ [in CBPV.CBV.DenotationalSemantics]
_ ≃v _ [in CBPV.CBV.DenotationalSemantics]
_ ≫* _ [in CBPV.CBV.DenotationalSemantics]
_ [[ _ ]] ⊢v _ : _ ; _ [in CBPV.CBV.DenotationalSemantics]
_ [[ _ ]] ⊩v _ : _ ; _ [in CBPV.CBV.DenotationalSemantics]
_ ↪ᵥ* _ [in CBPV.StrongReduction]
_ ↪* _ [in CBPV.StrongReduction]
_ ↪ᵥ _ [in CBPV.StrongReduction]
_ ↪ _ [in CBPV.StrongReduction]
_ ⇒ᵥ _ [in CBPV.StrongReduction]
_ ⇒ _ [in CBPV.StrongReduction]
$$ <- _ ; _ [in CBPV.Eagerlet]
$ <- _ ; _ [in CBPV.Terms]
<{ _ }> [in CBPV.Terms]
•__c [in CBPV.ProgramContexts]
•__v [in CBPV.ProgramContexts]
• [in CBPV.CBN.DenotationalSemantics]
⟨ _ ; _ ⟩ [in CBPV.Terms]
Module Index
C
CommaNotation [in CBPV.fintype]Counterexample [in CBPV.CBV.strongStory]
Variable Index
C
ClosureRelations.R [in CBPV.AbstractReductionSystems]ClosureRelations.X [in CBPV.AbstractReductionSystems]
CompatibilityLemmas.A [in CBPV.LogicalEquivalence]
CompatibilityLemmas.A [in CBPV.StrongNormalisation]
CompatibilityLemmas.A1 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.A1 [in CBPV.StrongNormalisation]
CompatibilityLemmas.A2 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.A2 [in CBPV.StrongNormalisation]
CompatibilityLemmas.B [in CBPV.LogicalEquivalence]
CompatibilityLemmas.B [in CBPV.StrongNormalisation]
CompatibilityLemmas.B1 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.B1 [in CBPV.StrongNormalisation]
CompatibilityLemmas.B2 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.B2 [in CBPV.StrongNormalisation]
CompatibilityLemmas.c1 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c1' [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c2 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c2' [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c3 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c4 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c5 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c6 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c7 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.c8 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.n [in CBPV.LogicalEquivalence]
CompatibilityLemmas.n [in CBPV.StrongNormalisation]
CompatibilityLemmas.v1 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.v1' [in CBPV.LogicalEquivalence]
CompatibilityLemmas.v2 [in CBPV.LogicalEquivalence]
CompatibilityLemmas.v2' [in CBPV.LogicalEquivalence]
compatibility_lemmas.B2 [in CBPV.SemanticTyping]
compatibility_lemmas.B1 [in CBPV.SemanticTyping]
compatibility_lemmas.B [in CBPV.SemanticTyping]
compatibility_lemmas.A2 [in CBPV.SemanticTyping]
compatibility_lemmas.A1 [in CBPV.SemanticTyping]
compatibility_lemmas.A [in CBPV.SemanticTyping]
compatibility_lemmas.Gamma [in CBPV.SemanticTyping]
compatibility_lemmas.n [in CBPV.SemanticTyping]
Confluence.X [in CBPV.AbstractReductionSystems]
Counterexample.e [in CBPV.CBV.strongStory]
Counterexample.M [in CBPV.CBV.strongStory]
Counterexample.M' [in CBPV.CBV.strongStory]
D
DenotationalSemantics.T [in CBPV.DenotationalSemantics]Denotation.A [in CBPV.CBV.DenotationalSemantics]
Denotation.Gamma [in CBPV.CBV.DenotationalSemantics]
Denotation.mono_requirement [in CBPV.CBN.DenotationalSemantics]
Denotation.mono_requirement [in CBPV.CBV.DenotationalSemantics]
Denotation.n [in CBPV.CBV.DenotationalSemantics]
Denotation.T [in CBPV.CBN.DenotationalSemantics]
Denotation.T [in CBPV.CBV.DenotationalSemantics]
I
Iter.f [in CBPV.Base]Iter.X [in CBPV.Base]
L
LogicalRelation.mono_requirement [in CBPV.DenotationalSemantics]LogicalRelation.T [in CBPV.DenotationalSemantics]
P
Properties.X [in CBPV.AbstractReductionSystems]S
StrongNormalisation.A [in CBPV.AbstractReductionSystems]StrongNormalisation.R [in CBPV.AbstractReductionSystems]
StrongNormalisation.S [in CBPV.AbstractReductionSystems]
StrongNormalisation.X [in CBPV.AbstractReductionSystems]
T
Takahashi.R [in CBPV.TMT]Takahashi.rho [in CBPV.TMT]
Takahashi.tak [in CBPV.TMT]
Takahashi.X [in CBPV.TMT]
TAlgebra.T [in CBPV.DenotationalSemantics]
TMT.H1 [in CBPV.TMT]
TMT.H2 [in CBPV.TMT]
TMT.R [in CBPV.TMT]
TMT.S [in CBPV.TMT]
TMT.X [in CBPV.TMT]
TypingLemmas.A [in CBPV.StrongNormalisation]
TypingLemmas.A1 [in CBPV.StrongNormalisation]
TypingLemmas.A2 [in CBPV.StrongNormalisation]
TypingLemmas.B [in CBPV.StrongNormalisation]
TypingLemmas.B1 [in CBPV.StrongNormalisation]
TypingLemmas.B2 [in CBPV.StrongNormalisation]
TypingLemmas.Gamma [in CBPV.StrongNormalisation]
TypingLemmas.n [in CBPV.StrongNormalisation]
Library Index
A
AbstractReductionSystemsaxioms
B
BaseC
CBNCBN_CBPV
CBV
CBV_CBPV
Confluence
D
DenotationalSemanticsDenotationalSemantics
DenotationalSemantics
E
EagerletEquationalTheory
F
fintypeL
LogicalEquivalenceO
ObservationalEquivalenceP
ProgramContextsS
SemanticsSemanticTyping
StrongNormalisation
StrongReduction
strongStory
strongStory
SyntacticTyping
Syntax
T
TerminationTerms
TMT
W
weakStoryweakStory
Lemma Index
A
adequacy [in CBPV.DenotationalSemantics]Adequacy [in CBPV.CBN.DenotationalSemantics]
Adequacy [in CBPV.CBV.DenotationalSemantics]
adequacyᵥ [in CBPV.DenotationalSemantics]
Adequacyᵥ [in CBPV.CBV.DenotationalSemantics]
B
backwards [in CBPV.CBN.weakStory]backwards_evaluates [in CBPV.CBN.weakStory]
backwards_termination [in CBPV.CBV.strongStory]
backwards_termination [in CBPV.CBV.weakStory]
backwards_steps [in CBPV.CBV.weakStory]
backwards_step [in CBPV.CBV.weakStory]
backward_simulation [in CBPV.CBV.weakStory]
basic_lemma [in CBPV.DenotationalSemantics]
beta_step_preserved [in CBPV.CBN.strongStory]
beta_lift [in CBPV.Confluence]
beta₂_lift [in CBPV.Confluence]
bigstep_sn [in CBPV.Semantics]
bigstep_sn' [in CBPV.Semantics]
bigstep_normal [in CBPV.Semantics]
bigstep_functional [in CBPV.Semantics]
bigstep_prepend [in CBPV.Semantics]
bigstep_cons [in CBPV.Semantics]
bigstep_primitive_cons [in CBPV.Semantics]
bigstep_soundness [in CBPV.Semantics]
bind [in CBPV.LogicalEquivalence]
C
cbn_type_pres' [in CBPV.CBN.DenotationalSemantics]cbn_type_pres [in CBPV.CBN.CBN_CBPV]
cbn_typeVar' [in CBPV.CBN.CBN_CBPV]
church_rosser [in CBPV.AbstractReductionSystems]
ClosedSemanticSoundness [in CBPV.SemanticTyping]
closev_ren [in CBPV.StrongNormalisation]
closev_base [in CBPV.StrongNormalisation]
close_ren [in CBPV.StrongNormalisation]
close_base [in CBPV.StrongNormalisation]
close_red [in CBPV.StrongNormalisation]
close_sn [in CBPV.StrongNormalisation]
closure_under_reduction [in CBPV.LogicalEquivalence]
closure_under_expansion [in CBPV.LogicalEquivalence]
closure_ctx_red [in CBPV.DenotationalSemantics]
closure_ctx_eqv [in CBPV.DenotationalSemantics]
closure_under_expansion [in CBPV.SemanticTyping]
commute_caseS_lambda [in CBPV.EquationalTheory]
commute_let_app [in CBPV.EquationalTheory]
commute_let_tuple [in CBPV.EquationalTheory]
commute_let_lam [in CBPV.EquationalTheory]
commute_let_let [in CBPV.EquationalTheory]
compat_caseP [in CBPV.SemanticTyping]
compat_caseS [in CBPV.SemanticTyping]
compat_caseZ [in CBPV.SemanticTyping]
compat_force [in CBPV.SemanticTyping]
compat_proj [in CBPV.SemanticTyping]
compat_tuple [in CBPV.SemanticTyping]
compat_app [in CBPV.SemanticTyping]
compat_ret [in CBPV.SemanticTyping]
compat_letin [in CBPV.SemanticTyping]
compat_lambda [in CBPV.SemanticTyping]
compat_cone [in CBPV.SemanticTyping]
compat_thunk [in CBPV.SemanticTyping]
compat_sum [in CBPV.SemanticTyping]
compat_pair [in CBPV.SemanticTyping]
compat_unit [in CBPV.SemanticTyping]
compat_var [in CBPV.SemanticTyping]
compat_caseP [in CBPV.StrongNormalisation]
compat_caseS [in CBPV.StrongNormalisation]
compat_caseZ [in CBPV.StrongNormalisation]
compat_force [in CBPV.StrongNormalisation]
compat_proj [in CBPV.StrongNormalisation]
compat_tuple [in CBPV.StrongNormalisation]
compat_app [in CBPV.StrongNormalisation]
compat_ret [in CBPV.StrongNormalisation]
compat_letin [in CBPV.StrongNormalisation]
compat_lambda [in CBPV.StrongNormalisation]
compat_cone [in CBPV.StrongNormalisation]
compat_thunk [in CBPV.StrongNormalisation]
compat_sum [in CBPV.StrongNormalisation]
compat_pair [in CBPV.StrongNormalisation]
compat_unit [in CBPV.StrongNormalisation]
compat_var [in CBPV.StrongNormalisation]
compat_caseP_E [in CBPV.StrongNormalisation]
compat_caseS_E [in CBPV.StrongNormalisation]
compat_caseZ_E [in CBPV.StrongNormalisation]
compat_force_E [in CBPV.StrongNormalisation]
compat_proj_E [in CBPV.StrongNormalisation]
compat_tuple_E [in CBPV.StrongNormalisation]
compat_app_E [in CBPV.StrongNormalisation]
compat_ret_E [in CBPV.StrongNormalisation]
compat_letin_E [in CBPV.StrongNormalisation]
compat_lambda_E [in CBPV.StrongNormalisation]
compat_thunk_E [in CBPV.StrongNormalisation]
compat_sum_E [in CBPV.StrongNormalisation]
compat_pair_E [in CBPV.StrongNormalisation]
compComp_comp [in CBPV.Syntax]
compComp_value [in CBPV.Syntax]
compComp_exp [in CBPV.CBN.CBN]
compComp_Exp [in CBPV.CBV.CBV]
compComp_Value [in CBPV.CBV.CBV]
compComp'_comp [in CBPV.Syntax]
compComp'_value [in CBPV.Syntax]
compComp'_exp [in CBPV.CBN.CBN]
compComp'_Exp [in CBPV.CBV.CBV]
compComp'_Value [in CBPV.CBV.CBV]
compRen_comp [in CBPV.Syntax]
compRen_value [in CBPV.Syntax]
compRen_exp [in CBPV.CBN.CBN]
compRen_Exp [in CBPV.CBV.CBV]
compRen_Value [in CBPV.CBV.CBV]
compRen'_comp [in CBPV.Syntax]
compRen'_value [in CBPV.Syntax]
compRen'_exp [in CBPV.CBN.CBN]
compRen'_Exp [in CBPV.CBV.CBV]
compRen'_Value [in CBPV.CBV.CBV]
computation_typing_ext [in CBPV.CBN.CBN_CBPV]
comp_semeq_transitive [in CBPV.LogicalEquivalence]
comp_semeq_symmetry [in CBPV.LogicalEquivalence]
comp_evaluates [in CBPV.SemanticTyping]
comp_nf [in CBPV.SemanticTyping]
comp_obseq_cctx_congruence [in CBPV.ObservationalEquivalence]
comp_obseq_vctx_congruence [in CBPV.ObservationalEquivalence]
confluence [in CBPV.CBN.strongStory]
confluence [in CBPV.Confluence]
confluence_steps [in CBPV.Semantics]
confluence_unique_normal_forms [in CBPV.AbstractReductionSystems]
confluence_normal_right [in CBPV.AbstractReductionSystems]
confluence_normal_left [in CBPV.AbstractReductionSystems]
confluent_semi [in CBPV.AbstractReductionSystems]
congruence_caseP [in CBPV.LogicalEquivalence]
congruence_caseS [in CBPV.LogicalEquivalence]
congruence_caseZ [in CBPV.LogicalEquivalence]
congruence_proj [in CBPV.LogicalEquivalence]
congruence_eagerlet [in CBPV.LogicalEquivalence]
congruence_letin [in CBPV.LogicalEquivalence]
congruence_ret [in CBPV.LogicalEquivalence]
congruence_tuple [in CBPV.LogicalEquivalence]
congruence_app [in CBPV.LogicalEquivalence]
congruence_lambda [in CBPV.LogicalEquivalence]
congruence_force [in CBPV.LogicalEquivalence]
congruence_cu [in CBPV.LogicalEquivalence]
congruence_thunk [in CBPV.LogicalEquivalence]
congruence_inj [in CBPV.LogicalEquivalence]
congruence_pair [in CBPV.LogicalEquivalence]
congruence_u [in CBPV.LogicalEquivalence]
congr_caseP [in CBPV.Syntax]
congr_caseS [in CBPV.Syntax]
congr_caseZ [in CBPV.Syntax]
congr_proj [in CBPV.Syntax]
congr_letin [in CBPV.Syntax]
congr_ret [in CBPV.Syntax]
congr_tuple [in CBPV.Syntax]
congr_app [in CBPV.Syntax]
congr_lambda [in CBPV.Syntax]
congr_force [in CBPV.Syntax]
congr_cu [in CBPV.Syntax]
congr_thunk [in CBPV.Syntax]
congr_inj [in CBPV.Syntax]
congr_pair [in CBPV.Syntax]
congr_u [in CBPV.Syntax]
congr_arrow [in CBPV.Syntax]
congr_Pi [in CBPV.Syntax]
congr_F [in CBPV.Syntax]
congr_cone [in CBPV.Syntax]
congr_cross [in CBPV.Syntax]
congr_Sigma [in CBPV.Syntax]
congr_U [in CBPV.Syntax]
congr_one [in CBPV.Syntax]
congr_zero [in CBPV.Syntax]
congr_CaseS [in CBPV.CBN.CBN]
congr_Inj [in CBPV.CBN.CBN]
congr_Proj [in CBPV.CBN.CBN]
congr_Pair [in CBPV.CBN.CBN]
congr_App [in CBPV.CBN.CBN]
congr_Lam [in CBPV.CBN.CBN]
congr_One [in CBPV.CBN.CBN]
congr_Plus [in CBPV.CBN.CBN]
congr_Cross [in CBPV.CBN.CBN]
congr_Arr [in CBPV.CBN.CBN]
congr_Unit [in CBPV.CBN.CBN]
congr_CaseP [in CBPV.CBV.CBV]
congr_CaseS [in CBPV.CBV.CBV]
congr_App [in CBPV.CBV.CBV]
congr_Val [in CBPV.CBV.CBV]
congr_Inj [in CBPV.CBV.CBV]
congr_Pair [in CBPV.CBV.CBV]
congr_Lam [in CBPV.CBV.CBV]
congr_One [in CBPV.CBV.CBV]
congr_Plus [in CBPV.CBV.CBV]
congr_Cross [in CBPV.CBV.CBV]
congr_Arr [in CBPV.CBV.CBV]
congr_Unit [in CBPV.CBV.CBV]
cons_twice_ctx_subst [in CBPV.DenotationalSemantics]
cons_ctx_subst [in CBPV.DenotationalSemantics]
counted_exp [in CBPV.AbstractReductionSystems]
counted_trans [in CBPV.AbstractReductionSystems]
Counterexample.normal_e [in CBPV.CBV.strongStory]
Counterexample.not_normal_e [in CBPV.CBV.strongStory]
Counterexample.step1 [in CBPV.CBV.strongStory]
Counterexample.step2 [in CBPV.CBV.strongStory]
ctx_plus [in CBPV.Eagerlet]
ctx_plus_value [in CBPV.CBV.strongStory]
ctx_plus [in CBPV.CBV.strongStory]
D
denotation_context [in CBPV.DenotationalSemantics]denotation_of_groundtypes_inhabited [in CBPV.DenotationalSemantics]
denotation_termination [in CBPV.Termination]
destruct_comp_obseq [in CBPV.ObservationalEquivalence]
destruct_value_obseq [in CBPV.ObservationalEquivalence]
diamond_ext [in CBPV.AbstractReductionSystems]
diamond_confluent [in CBPV.AbstractReductionSystems]
diamond_semi_confluent [in CBPV.AbstractReductionSystems]
E
eagerlet_substcomp [in CBPV.Eagerlet]eagerlet_rencomp [in CBPV.Eagerlet]
eagerlet_ty [in CBPV.Eagerlet]
eagerlet_inv [in CBPV.Eagerlet]
ectx_compose [in CBPV.Semantics]
ectx_decompose [in CBPV.Semantics]
ectx_cctx_typing [in CBPV.CBN.DenotationalSemantics]
ectx_cctx [in CBPV.CBN.DenotationalSemantics]
equiv_soundness_CBVᵥ [in CBPV.EquationalTheory]
equiv_soundness_CBV [in CBPV.EquationalTheory]
equiv_soundness_CBN [in CBPV.EquationalTheory]
equiv_soundness_CBPVᵥ [in CBPV.EquationalTheory]
equiv_soundness_CBPV [in CBPV.EquationalTheory]
equiv_translation_CBVᵥ [in CBPV.EquationalTheory]
equiv_translation_CBV [in CBPV.EquationalTheory]
equiv_translation_CBN [in CBPV.EquationalTheory]
equiv_star [in CBPV.AbstractReductionSystems]
equiv_symm [in CBPV.AbstractReductionSystems]
equiv_trans [in CBPV.AbstractReductionSystems]
eta_caseP [in CBPV.EquationalTheory]
eta_caseS [in CBPV.EquationalTheory]
eta_pair [in CBPV.EquationalTheory]
eta_lambda [in CBPV.EquationalTheory]
eta_let [in CBPV.EquationalTheory]
eta_thunk [in CBPV.EquationalTheory]
eta_if'_typed [in CBPV.CBN.DenotationalSemantics]
eta_if_typed [in CBPV.CBN.DenotationalSemantics]
evaluates_backwards [in CBPV.CBN.strongStory]
evaluates_forward [in CBPV.CBN.strongStory]
evaluates_to [in CBPV.CBN.weakStory]
eval_evaluates [in CBPV.Semantics]
eval_bigstep [in CBPV.Semantics]
eval_eval'_true [in CBPV.CBN.DenotationalSemantics]
eval_eval' [in CBPV.CBN.DenotationalSemantics]
eval_subst_up_value_value [in CBPV.CBN.CBN_CBPV]
evaL_subst_ren [in CBPV.CBN.CBN_CBPV]
eval_subst_cons [in CBPV.CBN.CBN_CBPV]
eval_ctx_cons [in CBPV.CBN.CBN_CBPV]
eval_eval'_tt [in CBPV.CBV.DenotationalSemantics]
eval_eval' [in CBPV.CBV.DenotationalSemantics]
eval_ctx_cons [in CBPV.CBV.DenotationalSemantics]
E_transitive [in CBPV.LogicalEquivalence]
E_symmetry [in CBPV.LogicalEquivalence]
E_ind2 [in CBPV.StrongNormalisation]
E_ind [in CBPV.StrongNormalisation]
E_ren [in CBPV.StrongNormalisation]
F
fmap_funct [in CBPV.DenotationalSemantics]forward_simulation [in CBPV.CBV.weakStory]
fundamental_property_comp [in CBPV.LogicalEquivalence]
fundamental_property_value [in CBPV.LogicalEquivalence]
fundamental_property [in CBPV.LogicalEquivalence]
G
groundtypes_are_simple [in CBPV.LogicalEquivalence]ground_equiv [in CBPV.DenotationalSemantics]
G_cons [in CBPV.LogicalEquivalence]
G_transitive [in CBPV.LogicalEquivalence]
G_symmetry [in CBPV.LogicalEquivalence]
G_ext [in CBPV.StrongNormalisation]
G_ren [in CBPV.StrongNormalisation]
G_scons [in CBPV.StrongNormalisation]
G_id [in CBPV.StrongNormalisation]
I
injective_eval [in CBPV.CBV.CBV_CBPV]injective_renup [in CBPV.CBV.CBV_CBPV]
injective_shift [in CBPV.CBV.CBV_CBPV]
injective_eval [in CBPV.CBN.CBN_CBPV]
inj_star_inv [in CBPV.StrongReduction]
instId_comp [in CBPV.Syntax]
instId_value [in CBPV.Syntax]
instId_exp [in CBPV.CBN.CBN]
instId_Exp [in CBPV.CBV.CBV]
instId_Value [in CBPV.CBV.CBV]
it_shift [in CBPV.Base]
J
joinable_ext [in CBPV.AbstractReductionSystems]K
K_filled_typed [in CBPV.CBN.DenotationalSemantics]K_typed [in CBPV.CBN.DenotationalSemantics]
L
let_to_eagerlet [in CBPV.Eagerlet]logical_equivalence_strong_reduction_value_steps [in CBPV.LogicalEquivalence]
logical_equivalence_strong_reduction_steps [in CBPV.LogicalEquivalence]
logical_equivalence_weak_reduction_steps [in CBPV.LogicalEquivalence]
logical_equivalence_strong_reduction_value [in CBPV.LogicalEquivalence]
logical_equivalence_strong_reduction [in CBPV.LogicalEquivalence]
logical_equivalence_weak_reduction [in CBPV.LogicalEquivalence]
logical_equivalence_primitive_reduction [in CBPV.LogicalEquivalence]
logical_equivalence_obseq [in CBPV.LogicalEquivalence]
logical_equivalence_congruent_cctx_comp [in CBPV.LogicalEquivalence]
logical_equivalence_congruent_cctx_value [in CBPV.LogicalEquivalence]
logical_equivalence_congruent_vctx_comp [in CBPV.LogicalEquivalence]
logical_equivalence_congruent_vctx_value [in CBPV.LogicalEquivalence]
logical_equivalence_congruent [in CBPV.LogicalEquivalence]
logical_equivalence_Equivᵥ [in CBPV.EquationalTheory]
logical_equivalence_Equiv [in CBPV.EquationalTheory]
M
MStep_preserved [in CBPV.CBV.strongStory]MStep_preserved [in CBPV.CBV.weakStory]
mu_fmap [in CBPV.DenotationalSemantics]
N
nf_normal [in CBPV.Semantics]normalizing_extension [in CBPV.Semantics]
Normal_preserved' [in CBPV.CBN.weakStory]
Normal_preserved [in CBPV.CBN.weakStory]
Normal_nf [in CBPV.SemanticTyping]
normal_bigstep [in CBPV.Semantics]
normal_tt [in CBPV.CBN.DenotationalSemantics]
Normal_preserved [in CBPV.CBV.weakStory]
Normal_star_stops [in CBPV.AbstractReductionSystems]
Normal_SN [in CBPV.AbstractReductionSystems]
O
obseq_contains_steps [in CBPV.LogicalEquivalence]obseq_contains_step [in CBPV.LogicalEquivalence]
obseq_contains_pstep [in CBPV.LogicalEquivalence]
obseq_soundness [in CBPV.CBN.DenotationalSemantics]
obseq_soundness' [in CBPV.CBN.DenotationalSemantics]
obseq_soundnessᵥ [in CBPV.CBV.DenotationalSemantics]
obseq_soundness [in CBPV.CBV.DenotationalSemantics]
obseq_soundnessᵥ' [in CBPV.CBV.DenotationalSemantics]
obseq_soundness' [in CBPV.CBV.DenotationalSemantics]
P
parstepc_refl [in CBPV.Confluence]parstepv_refl [in CBPV.Confluence]
parstep_star_sstep [in CBPV.Confluence]
parstep_refl [in CBPV.Confluence]
pi [in CBPV.axioms]
plus_sstep_value_preserves [in CBPV.CBV.strongStory]
plus_fixpoint [in CBPV.AbstractReductionSystems]
plus_idem [in CBPV.AbstractReductionSystems]
plus_mono [in CBPV.AbstractReductionSystems]
plus_star_step [in CBPV.AbstractReductionSystems]
plus_destruct [in CBPV.AbstractReductionSystems]
plus_star [in CBPV.AbstractReductionSystems]
plus_exp [in CBPV.AbstractReductionSystems]
plus_trans [in CBPV.AbstractReductionSystems]
preservation [in CBPV.SyntacticTyping]
preservation_steps [in CBPV.SyntacticTyping]
primitive_preservation [in CBPV.SyntacticTyping]
progress [in CBPV.SyntacticTyping]
proper_eagerlet_plus_sstep_L [in CBPV.Eagerlet]
proper_eagerlet_sstep_L [in CBPV.Eagerlet]
proper_eagerlet_star_sstep [in CBPV.Eagerlet]
proper_subst_comp [in CBPV.StrongReduction]
pstep_subst [in CBPV.Semantics]
pstep_value_preserves_ren [in CBPV.CBV.strongStory]
pstep_anti_renaming [in CBPV.StrongReduction]
R
refines_steps [in CBPV.CBN.strongStory]refines_step [in CBPV.CBN.strongStory]
refines_to_eval [in CBPV.CBN.strongStory]
refines_steps [in CBPV.CBN.weakStory]
refines_step [in CBPV.CBN.weakStory]
refines_beta [in CBPV.CBN.weakStory]
refines_functional [in CBPV.CBN.CBN_CBPV]
refines_subst [in CBPV.CBN.CBN_CBPV]
refines_ren [in CBPV.CBN.CBN_CBPV]
refines_help [in CBPV.CBN.CBN_CBPV]
refl_steps [in CBPV.DenotationalSemantics]
refl_equiv [in CBPV.AbstractReductionSystems]
refl_star [in CBPV.AbstractReductionSystems]
renComp_comp [in CBPV.Syntax]
renComp_value [in CBPV.Syntax]
renComp_exp [in CBPV.CBN.CBN]
renComp_Exp [in CBPV.CBV.CBV]
renComp_Value [in CBPV.CBV.CBV]
renComp'_comp [in CBPV.Syntax]
renComp'_value [in CBPV.Syntax]
renComp'_exp [in CBPV.CBN.CBN]
renComp'_Exp [in CBPV.CBV.CBV]
renComp'_Value [in CBPV.CBV.CBV]
renRen_comp [in CBPV.Syntax]
renRen_value [in CBPV.Syntax]
renRen_exp [in CBPV.CBN.CBN]
renRen_Exp [in CBPV.CBV.CBV]
renRen_Value [in CBPV.CBV.CBV]
renRen'_comp [in CBPV.Syntax]
renRen'_value [in CBPV.Syntax]
renRen'_exp [in CBPV.CBN.CBN]
renRen'_Exp [in CBPV.CBV.CBV]
renRen'_Value [in CBPV.CBV.CBV]
ren_up_inj [in CBPV.CBN.CBN_CBPV]
ren_inj [in CBPV.CBN.CBN_CBPV]
ren_comp_eval [in CBPV.CBN.CBN_CBPV]
ren_lift [in CBPV.Confluence]
ren₂_lift [in CBPV.Confluence]
ret_plus_inv [in CBPV.CBV.strongStory]
ret_star_inv [in CBPV.StrongReduction]
rinstInst_comp [in CBPV.Syntax]
rinstInst_value [in CBPV.Syntax]
rinstInst_exp [in CBPV.CBN.CBN]
rinstInst_Exp [in CBPV.CBV.CBV]
rinstInst_Value [in CBPV.CBV.CBV]
S
sandwich_confluent [in CBPV.TMT]sandwich_equiv [in CBPV.TMT]
scons_comp [in CBPV.fintype]
scons_eta_id [in CBPV.fintype]
scons_eta [in CBPV.fintype]
SemanticSoundness [in CBPV.SemanticTyping]
SemanticSoundness [in CBPV.StrongNormalisation]
SN_CBN [in CBPV.CBN.strongStory]
SN_CBV [in CBPV.CBV.strongStory]
SN_CBVᵥ [in CBPV.CBV.strongStory]
SN_finite_steps [in CBPV.AbstractReductionSystems]
SN_morphism [in CBPV.AbstractReductionSystems]
SN_plus [in CBPV.AbstractReductionSystems]
SN_unfold [in CBPV.AbstractReductionSystems]
SN_ext [in CBPV.AbstractReductionSystems]
soundness [in CBPV.DenotationalSemantics]
ssteps_preservation [in CBPV.StrongReduction]
sstep_value_preserves_ren [in CBPV.CBV.strongStory]
sstep_value_confluent [in CBPV.Confluence]
sstep_confluent [in CBPV.Confluence]
sstep_preservation [in CBPV.StrongReduction]
sstep_progress [in CBPV.StrongReduction]
sstep_strong_step_value [in CBPV.StrongReduction]
sstep_strong_step [in CBPV.StrongReduction]
starstep_functional_nf [in CBPV.Semantics]
star_starL [in CBPV.AbstractReductionSystems]
star_absorbtion [in CBPV.AbstractReductionSystems]
star_idem [in CBPV.AbstractReductionSystems]
star_closure [in CBPV.AbstractReductionSystems]
star_mono [in CBPV.AbstractReductionSystems]
star_exp [in CBPV.AbstractReductionSystems]
star_trans [in CBPV.AbstractReductionSystems]
Steps_backwards [in CBPV.CBN.strongStory]
Steps_preserved [in CBPV.CBN.strongStory]
Steps_preserved [in CBPV.CBN.weakStory]
steps_bigstep [in CBPV.Semantics]
steps_nf_eval [in CBPV.Semantics]
stepv_thunk_inv [in CBPV.StrongReduction]
stepv_inj_inv [in CBPV.StrongReduction]
stepv_pair_inv [in CBPV.StrongReduction]
stepv_u_inv [in CBPV.StrongReduction]
stepv_var_inv [in CBPV.StrongReduction]
Step_inj_inv [in CBPV.CBN.strongStory]
Step_preserved [in CBPV.CBN.strongStory]
Step_preserved_refines [in CBPV.CBN.weakStory]
Step_preserved [in CBPV.CBN.weakStory]
step_equiv [in CBPV.Semantics]
step_functional [in CBPV.Semantics]
Step_preserved [in CBPV.CBV.weakStory]
step_star_plus [in CBPV.AbstractReductionSystems]
step_ren_comp_inv [in CBPV.StrongReduction]
step_caseP_inv [in CBPV.StrongReduction]
step_caseS_inv [in CBPV.StrongReduction]
step_caseZ_inv [in CBPV.StrongReduction]
step_proj_inv [in CBPV.StrongReduction]
step_letin_inv [in CBPV.StrongReduction]
step_ret_inv [in CBPV.StrongReduction]
step_tuple_inv [in CBPV.StrongReduction]
step_app_inv [in CBPV.StrongReduction]
step_lambda_inv [in CBPV.StrongReduction]
step_force_inv [in CBPV.StrongReduction]
step_cu_inv [in CBPV.StrongReduction]
step_strong [in CBPV.StrongReduction]
strong_normalisation [in CBPV.StrongNormalisation]
strong_normalisation_cbv [in CBPV.Termination]
strong_normalisation_cbvᵥ [in CBPV.Termination]
strong_normalisation_cbn [in CBPV.Termination]
strong_normalisation_cbpvᵥ [in CBPV.Termination]
strong_normalisation_cbpv [in CBPV.Termination]
strong_step_value_anti_renaming [in CBPV.StrongReduction]
strong_step_anti_renaming [in CBPV.StrongReduction]
strong_step_value_subst [in CBPV.StrongReduction]
strong_step_subst [in CBPV.StrongReduction]
strong_step_value_preservation [in CBPV.StrongReduction]
strong_step_preservation [in CBPV.StrongReduction]
strong_step_progress [in CBPV.StrongReduction]
strong_step_value_congruence_value [in CBPV.StrongReduction]
strong_step_value_congruence [in CBPV.StrongReduction]
strong_step_congruence_value [in CBPV.StrongReduction]
strong_step_congruence [in CBPV.StrongReduction]
subst_pres [in CBPV.CBN.strongStory]
subst_pointwise [in CBPV.CBN.strongStory]
sym_symmetric [in CBPV.AbstractReductionSystems]
T
takahashi [in CBPV.Confluence]tak_cofinal [in CBPV.TMT]
tak_mono_n [in CBPV.TMT]
tak_mono [in CBPV.TMT]
tak_sound [in CBPV.TMT]
tak_diamond [in CBPV.TMT]
terminal_step [in CBPV.CBN.strongStory]
thunk_star_inv [in CBPV.StrongReduction]
TMT [in CBPV.TMT]
trans_beta [in CBPV.CBN.weakStory]
trans_subst_exp [in CBPV.CBV.CBV_CBPV]
trans_subst_val [in CBPV.CBV.CBV_CBPV]
trans_subst_val' [in CBPV.CBV.CBV_CBPV]
trans_ren_exp [in CBPV.CBV.CBV_CBPV]
trans_ren_val [in CBPV.CBV.CBV_CBPV]
trans_ren_val' [in CBPV.CBV.CBV_CBPV]
trans_inj [in CBPV.CBN.CBN_CBPV]
trans_refines [in CBPV.CBN.CBN_CBPV]
trans_eval [in CBPV.CBN.CBN_CBPV]
trans_subst [in CBPV.CBN.CBN_CBPV]
trans_ren [in CBPV.CBN.CBN_CBPV]
trans_preserves [in CBPV.CBN.CBN_CBPV]
typepres_beta [in CBPV.SyntacticTyping]
typeVar' [in CBPV.SyntacticTyping]
U
up_ren_ren [in CBPV.fintype]V
val_semeq_transitive [in CBPV.LogicalEquivalence]val_semeq_symmetry [in CBPV.LogicalEquivalence]
val_obseq_cctx_congruence [in CBPV.ObservationalEquivalence]
val_obseq_vctx_congruence [in CBPV.ObservationalEquivalence]
varLRen_value [in CBPV.Syntax]
varLRen_exp [in CBPV.CBN.CBN]
varLRen_Value [in CBPV.CBV.CBV]
varL_value [in CBPV.Syntax]
varL_exp [in CBPV.CBN.CBN]
varL_Value [in CBPV.CBV.CBV]
VC_ren [in CBPV.StrongNormalisation]
VV_sn [in CBPV.StrongNormalisation]
VV_red [in CBPV.StrongNormalisation]
VV_var [in CBPV.StrongNormalisation]
VV_ren [in CBPV.StrongNormalisation]
V_C_transitive [in CBPV.LogicalEquivalence]
V_C_symmetry [in CBPV.LogicalEquivalence]
V_sn [in CBPV.StrongNormalisation]
V_sn_to_VV_sn [in CBPV.StrongNormalisation]
V_red [in CBPV.StrongNormalisation]
V_red_to_VV_red [in CBPV.StrongNormalisation]
W
weak_normalisation_cbv [in CBPV.Termination]weak_normalisation_cbn [in CBPV.Termination]
weak_normalisation_cbpv [in CBPV.Termination]
weak_simulation [in CBPV.CBV.weakStory]
WN_translates [in CBPV.CBN.weakStory]
WN_CBV [in CBPV.CBV.weakStory]
Constructor Index
A
app [in CBPV.Syntax]App [in CBPV.CBN.CBN]
App [in CBPV.CBV.CBV]
Arr [in CBPV.CBN.CBN]
Arr [in CBPV.CBV.CBV]
arrow [in CBPV.Syntax]
arrow [in CBPV.Terms]
B
bigstepApp [in CBPV.Semantics]bigstepCaseP [in CBPV.Semantics]
bigstepCaseS [in CBPV.Semantics]
bigstepCu [in CBPV.Semantics]
bigstepForce [in CBPV.Semantics]
bigstepLambda [in CBPV.Semantics]
bigstepLetin [in CBPV.Semantics]
bigstepProj [in CBPV.Semantics]
bigstepReturn [in CBPV.Semantics]
bigstepTuple [in CBPV.Semantics]
C
caseP [in CBPV.Syntax]CaseP [in CBPV.CBV.CBV]
caseS [in CBPV.Syntax]
CaseS [in CBPV.CBN.CBN]
CaseS [in CBPV.CBV.CBV]
caseZ [in CBPV.Syntax]
cbn_typeApp [in CBPV.CBN.CBN_CBPV]
cbn_typeCaseS [in CBPV.CBN.CBN_CBPV]
cbn_typeInj [in CBPV.CBN.CBN_CBPV]
cbn_typeProj [in CBPV.CBN.CBN_CBPV]
cbn_typePair [in CBPV.CBN.CBN_CBPV]
cbn_typeLam [in CBPV.CBN.CBN_CBPV]
cbn_typeUnit [in CBPV.CBN.CBN_CBPV]
cbn_typeVar [in CBPV.CBN.CBN_CBPV]
cctxAppL [in CBPV.ProgramContexts]
cctxAppR [in CBPV.ProgramContexts]
cctxCasePC [in CBPV.ProgramContexts]
cctxCasePV [in CBPV.ProgramContexts]
cctxCaseSL [in CBPV.ProgramContexts]
cctxCaseSR [in CBPV.ProgramContexts]
cctxCaseSV [in CBPV.ProgramContexts]
cctxCaseZ [in CBPV.ProgramContexts]
cctxForce [in CBPV.ProgramContexts]
cctxHole [in CBPV.ProgramContexts]
cctxLambda [in CBPV.ProgramContexts]
cctxLetinL [in CBPV.ProgramContexts]
cctxLetinR [in CBPV.ProgramContexts]
cctxProj [in CBPV.ProgramContexts]
cctxRet [in CBPV.ProgramContexts]
cctxTupleL [in CBPV.ProgramContexts]
cctxTupleR [in CBPV.ProgramContexts]
cctxTypingAppL [in CBPV.ProgramContexts]
cctxTypingAppR [in CBPV.ProgramContexts]
cctxTypingCasePC [in CBPV.ProgramContexts]
cctxTypingCasePV [in CBPV.ProgramContexts]
cctxTypingCaseSL [in CBPV.ProgramContexts]
cctxTypingCaseSR [in CBPV.ProgramContexts]
cctxTypingCaseSV [in CBPV.ProgramContexts]
cctxTypingCaseZ [in CBPV.ProgramContexts]
cctxTypingForce [in CBPV.ProgramContexts]
cctxTypingHole [in CBPV.ProgramContexts]
cctxTypingLambda [in CBPV.ProgramContexts]
cctxTypingLetinL [in CBPV.ProgramContexts]
cctxTypingLetinR [in CBPV.ProgramContexts]
cctxTypingProj [in CBPV.ProgramContexts]
cctxTypingRet [in CBPV.ProgramContexts]
cctxTypingTupleL [in CBPV.ProgramContexts]
cctxTypingTupleR [in CBPV.ProgramContexts]
cctxᵥAppL [in CBPV.CBV.DenotationalSemantics]
cctxᵥAppR [in CBPV.CBV.DenotationalSemantics]
cctxᵥCasePC [in CBPV.CBV.DenotationalSemantics]
cctxᵥCasePV [in CBPV.CBV.DenotationalSemantics]
cctxᵥCaseSL [in CBPV.CBV.DenotationalSemantics]
cctxᵥCaseSR [in CBPV.CBV.DenotationalSemantics]
cctxᵥCaseSV [in CBPV.CBV.DenotationalSemantics]
cctxᵥHole [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingAppL [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingAppR [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCasePC [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCasePV [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCaseSL [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCaseSR [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingCaseSV [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingHole [in CBPV.CBV.DenotationalSemantics]
cctxᵥTypingVctx [in CBPV.CBV.DenotationalSemantics]
cctxᵥVctx [in CBPV.CBV.DenotationalSemantics]
closev_V [in CBPV.StrongNormalisation]
closev_var [in CBPV.StrongNormalisation]
close_step [in CBPV.StrongNormalisation]
cone [in CBPV.Syntax]
cone [in CBPV.Terms]
contextStep [in CBPV.Semantics]
countedRefl [in CBPV.AbstractReductionSystems]
countedStep [in CBPV.AbstractReductionSystems]
cross [in CBPV.Syntax]
cross [in CBPV.Terms]
Cross [in CBPV.CBN.CBN]
Cross [in CBPV.CBV.CBV]
cu [in CBPV.Syntax]
E
ectxApp [in CBPV.Semantics]ectxAppL [in CBPV.CBN.DenotationalSemantics]
ectxAppR [in CBPV.CBN.DenotationalSemantics]
ectxCaseSL [in CBPV.CBN.DenotationalSemantics]
ectxCaseSR [in CBPV.CBN.DenotationalSemantics]
ectxCaseSV [in CBPV.CBN.DenotationalSemantics]
ectxHole [in CBPV.Semantics]
ectxHole [in CBPV.CBN.DenotationalSemantics]
ectxInj [in CBPV.CBN.DenotationalSemantics]
ectxLambda [in CBPV.CBN.DenotationalSemantics]
ectxLetin [in CBPV.Semantics]
ectxPairL [in CBPV.CBN.DenotationalSemantics]
ectxPairR [in CBPV.CBN.DenotationalSemantics]
ectxProj [in CBPV.Semantics]
ectxProj [in CBPV.CBN.DenotationalSemantics]
ectxTypingAppL [in CBPV.CBN.DenotationalSemantics]
ectxTypingAppR [in CBPV.CBN.DenotationalSemantics]
ectxTypingCaseSL [in CBPV.CBN.DenotationalSemantics]
ectxTypingCaseSR [in CBPV.CBN.DenotationalSemantics]
ectxTypingCaseSV [in CBPV.CBN.DenotationalSemantics]
ectxTypingHole [in CBPV.CBN.DenotationalSemantics]
ectxTypingInj [in CBPV.CBN.DenotationalSemantics]
ectxTypingLambda [in CBPV.CBN.DenotationalSemantics]
ectxTypingPairL [in CBPV.CBN.DenotationalSemantics]
ectxTypingPairR [in CBPV.CBN.DenotationalSemantics]
ectxTypingProj [in CBPV.CBN.DenotationalSemantics]
F
F [in CBPV.Syntax]F [in CBPV.Terms]
force [in CBPV.Syntax]
G
gcross [in CBPV.Terms]gone [in CBPV.Terms]
gsum [in CBPV.Terms]
I
ids [in CBPV.fintype]inhabited [in CBPV.Base]
inj [in CBPV.Syntax]
Inj [in CBPV.CBN.CBN]
Inj [in CBPV.CBV.CBV]
L
Lam [in CBPV.CBN.CBN]Lam [in CBPV.CBV.CBV]
lambda [in CBPV.Syntax]
letin [in CBPV.Syntax]
M
mkCBN [in CBPV.CBN.DenotationalSemantics]mkCBPVc [in CBPV.ObservationalEquivalence]
mkCBPVv [in CBPV.ObservationalEquivalence]
mkCBV [in CBPV.CBV.DenotationalSemantics]
mkCBVᵥ [in CBPV.CBV.DenotationalSemantics]
N
nfCu [in CBPV.Semantics]nfLam [in CBPV.Semantics]
nfRet [in CBPV.Semantics]
nfTup [in CBPV.Semantics]
O
one [in CBPV.Syntax]one [in CBPV.Terms]
One [in CBPV.CBN.CBN]
One [in CBPV.CBV.CBV]
P
pair [in CBPV.Syntax]Pair [in CBPV.CBN.CBN]
Pair [in CBPV.CBV.CBV]
parstepcApp [in CBPV.Confluence]
parstepcAppBeta [in CBPV.Confluence]
parstepcCaseP [in CBPV.Confluence]
parstepcCasePBeta [in CBPV.Confluence]
parstepcCaseS [in CBPV.Confluence]
parstepcCaseSBeta [in CBPV.Confluence]
parstepcCaseZ [in CBPV.Confluence]
parstepcCu [in CBPV.Confluence]
parstepcForce [in CBPV.Confluence]
parstepcForceBeta [in CBPV.Confluence]
parstepcLambda [in CBPV.Confluence]
parstepcLetin [in CBPV.Confluence]
parstepcLetinBeta [in CBPV.Confluence]
parstepcProj [in CBPV.Confluence]
parstepcProjBeta [in CBPV.Confluence]
parstepcRet [in CBPV.Confluence]
parstepcTuple [in CBPV.Confluence]
parstepvInj [in CBPV.Confluence]
parstepvPair [in CBPV.Confluence]
parstepvThunk [in CBPV.Confluence]
parstepvU [in CBPV.Confluence]
parstepvVar [in CBPV.Confluence]
Pi [in CBPV.Syntax]
Pi [in CBPV.Terms]
Plus [in CBPV.CBN.CBN]
Plus [in CBPV.CBV.CBV]
plusSingle [in CBPV.AbstractReductionSystems]
plusStep [in CBPV.AbstractReductionSystems]
proj [in CBPV.Syntax]
Proj [in CBPV.CBN.CBN]
pstepApp [in CBPV.Semantics]
pstepCaseP [in CBPV.Semantics]
pstepCaseS [in CBPV.Semantics]
pstepForce [in CBPV.Semantics]
pstepLetin [in CBPV.Semantics]
pstepProj [in CBPV.Semantics]
R
refines_FT [in CBPV.CBN.CBN_CBPV]refines_CaseS2 [in CBPV.CBN.CBN_CBPV]
refines_CaseS [in CBPV.CBN.CBN_CBPV]
refines_Inj [in CBPV.CBN.CBN_CBPV]
refines_Proj [in CBPV.CBN.CBN_CBPV]
refines_Pair [in CBPV.CBN.CBN_CBPV]
refines_App [in CBPV.CBN.CBN_CBPV]
refines_Lam [in CBPV.CBN.CBN_CBPV]
refines_One [in CBPV.CBN.CBN_CBPV]
refines_var [in CBPV.CBN.CBN_CBPV]
ren1 [in CBPV.fintype]
ren2 [in CBPV.fintype]
ret [in CBPV.Syntax]
S
Sigma [in CBPV.Syntax]Sigma [in CBPV.Terms]
SNC [in CBPV.AbstractReductionSystems]
sstepAppL [in CBPV.StrongReduction]
sstepAppR [in CBPV.StrongReduction]
sstepCasePC [in CBPV.StrongReduction]
sstepCasePV [in CBPV.StrongReduction]
sstepCaseSL [in CBPV.StrongReduction]
sstepCaseSR [in CBPV.StrongReduction]
sstepCaseSV [in CBPV.StrongReduction]
sstepCaseZ [in CBPV.StrongReduction]
sstepForce [in CBPV.StrongReduction]
sstepLambda [in CBPV.StrongReduction]
sstepLetinL [in CBPV.StrongReduction]
sstepLetinR [in CBPV.StrongReduction]
sstepPrimitive [in CBPV.StrongReduction]
sstepProj [in CBPV.StrongReduction]
sstepRet [in CBPV.StrongReduction]
sstepTupleL [in CBPV.StrongReduction]
sstepTupleR [in CBPV.StrongReduction]
sstepValueInj [in CBPV.StrongReduction]
sstepValuePairL [in CBPV.StrongReduction]
sstepValuePairR [in CBPV.StrongReduction]
sstepValueThunk [in CBPV.StrongReduction]
starRefl [in CBPV.AbstractReductionSystems]
starReflL [in CBPV.AbstractReductionSystems]
starStep [in CBPV.AbstractReductionSystems]
starStepL [in CBPV.AbstractReductionSystems]
stepApp [in CBPV.Semantics]
StepAppLam [in CBPV.CBN.strongStory]
StepAppLam [in CBPV.CBN.weakStory]
StepAppLam [in CBPV.CBV.strongStory]
StepAppLam [in CBPV.CBV.weakStory]
StepApp1 [in CBPV.CBN.strongStory]
StepApp1 [in CBPV.CBN.weakStory]
StepApp1 [in CBPV.CBV.strongStory]
StepApp1 [in CBPV.CBV.weakStory]
StepApp2 [in CBPV.CBN.strongStory]
StepApp2 [in CBPV.CBV.strongStory]
StepApp2 [in CBPV.CBV.weakStory]
StepCaseP [in CBPV.CBV.strongStory]
StepCaseP [in CBPV.CBV.weakStory]
StepCaseP1 [in CBPV.CBV.strongStory]
StepCaseP1 [in CBPV.CBV.weakStory]
StepCaseP2 [in CBPV.CBV.strongStory]
StepCaseS [in CBPV.CBN.strongStory]
StepCaseS [in CBPV.CBN.weakStory]
StepCaseS [in CBPV.CBV.strongStory]
StepCaseS [in CBPV.CBV.weakStory]
StepCaseS1 [in CBPV.CBN.strongStory]
StepCaseS1 [in CBPV.CBN.weakStory]
StepCaseS1 [in CBPV.CBV.strongStory]
StepCaseS1 [in CBPV.CBV.weakStory]
StepCaseS2 [in CBPV.CBN.strongStory]
StepCaseS2 [in CBPV.CBV.strongStory]
StepCaseS3 [in CBPV.CBN.strongStory]
StepCaseS3 [in CBPV.CBV.strongStory]
StepInj [in CBPV.CBN.strongStory]
StepInj [in CBPV.CBV.strongStory]
StepLam [in CBPV.CBN.strongStory]
StepLam [in CBPV.CBV.strongStory]
stepLetin [in CBPV.Semantics]
StepPair1 [in CBPV.CBN.strongStory]
StepPair1 [in CBPV.CBV.strongStory]
StepPair2 [in CBPV.CBN.strongStory]
StepPair2 [in CBPV.CBV.strongStory]
stepPrimitive [in CBPV.Semantics]
StepProj [in CBPV.CBN.strongStory]
StepProj [in CBPV.CBN.weakStory]
stepProj [in CBPV.Semantics]
StepProjPair [in CBPV.CBN.strongStory]
StepProjPair [in CBPV.CBN.weakStory]
StepValue [in CBPV.CBV.strongStory]
strong_reduce_value [in CBPV.StrongReduction]
strong_reduce [in CBPV.StrongReduction]
subst1 [in CBPV.fintype]
subst2 [in CBPV.fintype]
symId [in CBPV.AbstractReductionSystems]
symInv [in CBPV.AbstractReductionSystems]
T
thunk [in CBPV.Syntax]trans_FT [in CBPV.CBN.CBN_CBPV]
trans_CaseS [in CBPV.CBN.CBN_CBPV]
trans_Inj [in CBPV.CBN.CBN_CBPV]
trans_Proj [in CBPV.CBN.CBN_CBPV]
trans_Pair [in CBPV.CBN.CBN_CBPV]
trans_App [in CBPV.CBN.CBN_CBPV]
trans_Lam [in CBPV.CBN.CBN_CBPV]
trans_One [in CBPV.CBN.CBN_CBPV]
trans_var [in CBPV.CBN.CBN_CBPV]
tuple [in CBPV.Syntax]
typeApp [in CBPV.CBV.CBV_CBPV]
typeApp [in CBPV.SyntacticTyping]
typeCaseP [in CBPV.CBV.CBV_CBPV]
typeCaseP [in CBPV.SyntacticTyping]
typeCaseS [in CBPV.CBV.CBV_CBPV]
typeCaseS [in CBPV.SyntacticTyping]
typeCaseZ [in CBPV.SyntacticTyping]
typeCone [in CBPV.SyntacticTyping]
typeForce [in CBPV.SyntacticTyping]
typeInjL [in CBPV.CBV.CBV_CBPV]
typeLam [in CBPV.CBV.CBV_CBPV]
typeLambda [in CBPV.SyntacticTyping]
typeLetin [in CBPV.SyntacticTyping]
typeOne [in CBPV.CBV.CBV_CBPV]
typePair [in CBPV.CBV.CBV_CBPV]
typePair [in CBPV.SyntacticTyping]
typeProj [in CBPV.SyntacticTyping]
typeRet [in CBPV.SyntacticTyping]
typeSum [in CBPV.SyntacticTyping]
typeThunk [in CBPV.SyntacticTyping]
typeTuple [in CBPV.SyntacticTyping]
typeUnit [in CBPV.SyntacticTyping]
typeVal [in CBPV.CBV.CBV_CBPV]
typeVar [in CBPV.SyntacticTyping]
typeVarV [in CBPV.CBV.CBV_CBPV]
U
u [in CBPV.Syntax]U [in CBPV.Syntax]
U [in CBPV.Terms]
Unit [in CBPV.CBN.CBN]
Unit [in CBPV.CBV.CBV]
V
Val [in CBPV.CBV.CBV]var_value [in CBPV.Syntax]
var_exp [in CBPV.CBN.CBN]
var_Value [in CBPV.CBV.CBV]
vctxHole [in CBPV.ProgramContexts]
vctxInj [in CBPV.ProgramContexts]
vctxPairL [in CBPV.ProgramContexts]
vctxPairR [in CBPV.ProgramContexts]
vctxThunk [in CBPV.ProgramContexts]
vctxTypingHole [in CBPV.ProgramContexts]
vctxTypingInj [in CBPV.ProgramContexts]
vctxTypingPairL [in CBPV.ProgramContexts]
vctxTypingPairR [in CBPV.ProgramContexts]
vctxTypingThunk [in CBPV.ProgramContexts]
vctxᵥHole [in CBPV.CBV.DenotationalSemantics]
vctxᵥInj [in CBPV.CBV.DenotationalSemantics]
vctxᵥLambda [in CBPV.CBV.DenotationalSemantics]
vctxᵥPairL [in CBPV.CBV.DenotationalSemantics]
vctxᵥPairR [in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingHole [in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingInj [in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingLambda [in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingPairL [in CBPV.CBV.DenotationalSemantics]
vctxᵥTypingPairR [in CBPV.CBV.DenotationalSemantics]
Z
zero [in CBPV.Syntax]zero [in CBPV.Terms]
Axiom Index
P
pext [in CBPV.axioms]Inductive Index
B
bigstep [in CBPV.Semantics]C
cbn_typing [in CBPV.CBN.CBN_CBPV]cctx [in CBPV.ProgramContexts]
cctxTyping [in CBPV.ProgramContexts]
cctxᵥ [in CBPV.CBV.DenotationalSemantics]
cctxᵥTyping [in CBPV.CBV.DenotationalSemantics]
close [in CBPV.StrongNormalisation]
closev [in CBPV.StrongNormalisation]
comp [in CBPV.Syntax]
comptype [in CBPV.Syntax]
comptype [in CBPV.Terms]
computation_typing [in CBPV.SyntacticTyping]
counted [in CBPV.AbstractReductionSystems]
cstep [in CBPV.Semantics]
E
ectx [in CBPV.Semantics]ectx [in CBPV.CBN.DenotationalSemantics]
ectxTyping [in CBPV.CBN.DenotationalSemantics]
exp [in CBPV.CBN.CBN]
Exp [in CBPV.CBV.CBV]
G
groundtype [in CBPV.Terms]H
has_typeE [in CBPV.CBV.CBV_CBPV]has_typeV [in CBPV.CBV.CBV_CBPV]
I
inhab [in CBPV.Base]N
nf [in CBPV.Semantics]P
parstepc [in CBPV.Confluence]parstepv [in CBPV.Confluence]
plus [in CBPV.AbstractReductionSystems]
pstep [in CBPV.Semantics]
R
refines [in CBPV.CBN.CBN_CBPV]Ren1 [in CBPV.fintype]
Ren2 [in CBPV.fintype]
S
SN [in CBPV.AbstractReductionSystems]sstep [in CBPV.StrongReduction]
sstep_value [in CBPV.StrongReduction]
star [in CBPV.AbstractReductionSystems]
starL [in CBPV.AbstractReductionSystems]
Step [in CBPV.CBN.strongStory]
Step [in CBPV.CBN.weakStory]
step [in CBPV.Semantics]
Step [in CBPV.CBV.strongStory]
Step [in CBPV.CBV.weakStory]
StepVal [in CBPV.CBV.strongStory]
strong_step_value [in CBPV.StrongReduction]
strong_step [in CBPV.StrongReduction]
Subst1 [in CBPV.fintype]
Subst2 [in CBPV.fintype]
sym [in CBPV.AbstractReductionSystems]
T
trans [in CBPV.CBN.CBN_CBPV]type [in CBPV.CBN.CBN]
type [in CBPV.CBV.CBV]
V
valtype [in CBPV.Syntax]valtype [in CBPV.Terms]
value [in CBPV.Syntax]
Value [in CBPV.CBV.CBV]
value_typing [in CBPV.SyntacticTyping]
Var [in CBPV.fintype]
vctx [in CBPV.ProgramContexts]
vctxTyping [in CBPV.ProgramContexts]
vctxᵥ [in CBPV.CBV.DenotationalSemantics]
vctxᵥTyping [in CBPV.CBV.DenotationalSemantics]
Projection Index
A
algstruct [in CBPV.DenotationalSemantics]C
Carrier [in CBPV.DenotationalSemantics]CBN_H [in CBPV.CBN.DenotationalSemantics]
CBN_e [in CBPV.CBN.DenotationalSemantics]
CBPVc_H [in CBPV.ObservationalEquivalence]
CBPVc_c [in CBPV.ObservationalEquivalence]
CBPVv_H [in CBPV.ObservationalEquivalence]
CBPVv_v [in CBPV.ObservationalEquivalence]
CBV_Hᵥ [in CBPV.CBV.DenotationalSemantics]
CBV_v [in CBPV.CBV.DenotationalSemantics]
CBV_H [in CBPV.CBV.DenotationalSemantics]
CBV_e [in CBPV.CBV.DenotationalSemantics]
I
ids [in CBPV.fintype]M
mbind [in CBPV.DenotationalSemantics]monad1 [in CBPV.DenotationalSemantics]
monad2 [in CBPV.DenotationalSemantics]
monad3 [in CBPV.DenotationalSemantics]
mreturn [in CBPV.DenotationalSemantics]
P
parstep [in CBPV.Confluence]R
ren1 [in CBPV.fintype]ren2 [in CBPV.fintype]
S
subst1 [in CBPV.fintype]subst2 [in CBPV.fintype]
T
T [in CBPV.DenotationalSemantics]t_algebra2 [in CBPV.DenotationalSemantics]
t_algebra1 [in CBPV.DenotationalSemantics]
Instance Index
C
comp_semeq_trans [in CBPV.LogicalEquivalence]comp_semeq_symm [in CBPV.LogicalEquivalence]
C_trans [in CBPV.LogicalEquivalence]
C_symm [in CBPV.LogicalEquivalence]
E
equiv_exp_obseq [in CBPV.CBN.DenotationalSemantics]equiv_comp_obseq [in CBPV.ObservationalEquivalence]
equiv_value_obseq [in CBPV.ObservationalEquivalence]
equiv_Equivalence [in CBPV.AbstractReductionSystems]
equiv_value_obseq [in CBPV.CBV.DenotationalSemantics]
equiv_exp_obseq [in CBPV.CBV.DenotationalSemantics]
E_trans [in CBPV.LogicalEquivalence]
E_symm [in CBPV.LogicalEquivalence]
G
G_trans [in CBPV.LogicalEquivalence]G_symm [in CBPV.LogicalEquivalence]
P
parstep_comp [in CBPV.Confluence]parstep_value [in CBPV.Confluence]
plus_proper_sstep_letinL' [in CBPV.CBV.strongStory]
plus_transitive [in CBPV.AbstractReductionSystems]
plus_expansive [in CBPV.AbstractReductionSystems]
plus_sstep_preserves [in CBPV.StrongReduction]
plus_proper_sstep_caseP2 [in CBPV.StrongReduction]
plus_proper_sstep_caseP1 [in CBPV.StrongReduction]
plus_proper_sstep_caseS3 [in CBPV.StrongReduction]
plus_proper_sstep_caseS2 [in CBPV.StrongReduction]
plus_proper_sstep_caseS1 [in CBPV.StrongReduction]
plus_proper_sstep_proj [in CBPV.StrongReduction]
plus_proper_sstep_letinR [in CBPV.StrongReduction]
plus_proper_sstep_letinL [in CBPV.StrongReduction]
plus_proper_sstep_ret [in CBPV.StrongReduction]
plus_proper_sstep_tupleR [in CBPV.StrongReduction]
plus_proper_sstep_tupleL [in CBPV.StrongReduction]
plus_proper_sstep_appR [in CBPV.StrongReduction]
plus_proper_sstep_appL [in CBPV.StrongReduction]
plus_proper_sstep_lambda [in CBPV.StrongReduction]
plus_proper_sstep_force [in CBPV.StrongReduction]
plus_proper_sstep_thunk [in CBPV.StrongReduction]
plus_proper_sstep_inj [in CBPV.StrongReduction]
plus_proper_sstep_pairR [in CBPV.StrongReduction]
plus_proper_sstep_pairL [in CBPV.StrongReduction]
proper_Step_Case3 [in CBPV.CBN.strongStory]
proper_Step_Case2 [in CBPV.CBN.strongStory]
proper_Step_Case [in CBPV.CBN.strongStory]
proper_Step_Inj [in CBPV.CBN.strongStory]
proper_Step_Proj [in CBPV.CBN.strongStory]
proper_Step_Lam [in CBPV.CBN.strongStory]
proper_Step_App2 [in CBPV.CBN.strongStory]
proper_Step_App [in CBPV.CBN.strongStory]
proper_Step_Pair2 [in CBPV.CBN.strongStory]
proper_Step_Pair [in CBPV.CBN.strongStory]
proper_Step_Case [in CBPV.CBN.weakStory]
proper_Step_Proj [in CBPV.CBN.weakStory]
proper_Step_App [in CBPV.CBN.weakStory]
proper_eagerlet_star_sstep_L [in CBPV.Eagerlet]
proper_eagerlet_sstep_L_star [in CBPV.Eagerlet]
proper_eagerlet_plus_sstep_R [in CBPV.Eagerlet]
proper_eagerlet_star_ssstep_R [in CBPV.Eagerlet]
proper_eagerlet_sstep_R [in CBPV.Eagerlet]
proper_eagerlet_plus_step_L [in CBPV.Eagerlet]
proper_eagerlet_star_step_L [in CBPV.Eagerlet]
proper_proj [in CBPV.Semantics]
proper_app [in CBPV.Semantics]
proper_letin [in CBPV.Semantics]
proper_Step_Pair [in CBPV.CBV.strongStory]
proper_Step_Lam [in CBPV.CBV.strongStory]
proper_Step_Inj [in CBPV.CBV.strongStory]
proper_Step_Val [in CBPV.CBV.strongStory]
proper_Step_CaseP [in CBPV.CBV.strongStory]
proper_Step_Case [in CBPV.CBV.strongStory]
proper_Step_App [in CBPV.CBV.strongStory]
proper_Step_CaseP [in CBPV.CBV.weakStory]
proper_Step_Case [in CBPV.CBV.weakStory]
proper_Step_App [in CBPV.CBV.weakStory]
proper_sstep_caseP2 [in CBPV.StrongReduction]
proper_sstep_caseP1 [in CBPV.StrongReduction]
proper_sstep_caseS3 [in CBPV.StrongReduction]
proper_sstep_caseS2 [in CBPV.StrongReduction]
proper_sstep_caseS1 [in CBPV.StrongReduction]
proper_sstep_caseZ [in CBPV.StrongReduction]
proper_sstep_proj [in CBPV.StrongReduction]
proper_sstep_letinR [in CBPV.StrongReduction]
proper_sstep_letinL [in CBPV.StrongReduction]
proper_sstep_ret [in CBPV.StrongReduction]
proper_sstep_tupleR [in CBPV.StrongReduction]
proper_sstep_tupleL [in CBPV.StrongReduction]
proper_sstep_appR [in CBPV.StrongReduction]
proper_sstep_appL [in CBPV.StrongReduction]
proper_sstep_lambda [in CBPV.StrongReduction]
proper_sstep_force [in CBPV.StrongReduction]
proper_sstep_thunk [in CBPV.StrongReduction]
proper_sstep_inj [in CBPV.StrongReduction]
proper_sstep_pairR [in CBPV.StrongReduction]
proper_sstep_pairL [in CBPV.StrongReduction]
pstep_subrel [in CBPV.StrongReduction]
R
Ren_comp [in CBPV.Syntax]Ren_value [in CBPV.Syntax]
Ren_exp [in CBPV.CBN.CBN]
Ren_Exp [in CBPV.CBV.CBV]
Ren_Value [in CBPV.CBV.CBV]
ren_value_proper [in CBPV.StrongReduction]
ren_comp_proper [in CBPV.StrongReduction]
S
star_expansive [in CBPV.AbstractReductionSystems]star_preorder [in CBPV.AbstractReductionSystems]
star_sstep_preserves_value [in CBPV.StrongReduction]
star_sstep_preserves [in CBPV.StrongReduction]
subrel_C_E [in CBPV.LogicalEquivalence]
subrel_star_equiv [in CBPV.AbstractReductionSystems]
subrel_plus_mono [in CBPV.AbstractReductionSystems]
subrel_star_mono [in CBPV.AbstractReductionSystems]
subrel_star [in CBPV.AbstractReductionSystems]
subrel_step_sstep [in CBPV.StrongReduction]
Subst_comp [in CBPV.Syntax]
Subst_value [in CBPV.Syntax]
Subst_exp [in CBPV.CBN.CBN]
Subst_Exp [in CBPV.CBV.CBV]
Subst_Value [in CBPV.CBV.CBV]
sym_Symmetric [in CBPV.AbstractReductionSystems]
V
val_semeq_trans [in CBPV.LogicalEquivalence]val_semeq_symm [in CBPV.LogicalEquivalence]
VarInstance_value [in CBPV.Syntax]
VarInstance_exp [in CBPV.CBN.CBN]
VarInstance_Value [in CBPV.CBV.CBV]
V_trans [in CBPV.LogicalEquivalence]
V_symm [in CBPV.LogicalEquivalence]
Section Index
C
ClosureRelations [in CBPV.AbstractReductionSystems]CompatibilityLemmas [in CBPV.LogicalEquivalence]
CompatibilityLemmas [in CBPV.StrongNormalisation]
compatibility_lemmas [in CBPV.SemanticTyping]
Confluence [in CBPV.AbstractReductionSystems]
D
Denotation [in CBPV.CBN.DenotationalSemantics]Denotation [in CBPV.CBV.DenotationalSemantics]
DenotationalSemantics [in CBPV.DenotationalSemantics]
I
Iter [in CBPV.Base]L
LogicalRelation [in CBPV.DenotationalSemantics]O
ObservationalEquivalenceSoundness [in CBPV.CBN.DenotationalSemantics]ObservationalEquivalenceSoundness [in CBPV.CBV.DenotationalSemantics]
P
Properties [in CBPV.AbstractReductionSystems]S
StrongNormalisation [in CBPV.AbstractReductionSystems]T
Takahashi [in CBPV.TMT]TAlgebra [in CBPV.DenotationalSemantics]
TMT [in CBPV.TMT]
TypingLemmas [in CBPV.StrongNormalisation]
Abbreviation Index
E
E [in CBPV.LogicalEquivalence]E [in CBPV.SemanticTyping]
E [in CBPV.StrongNormalisation]
I
injective [in CBPV.CBN.CBN_CBPV]R
ren_up [in CBPV.CBN.CBN_CBPV]U
up_ren [in CBPV.CBV.CBV_CBPV]up2_ren [in CBPV.CBV.CBV_CBPV]
V
VV [in CBPV.StrongNormalisation]other
η [in CBPV.DenotationalSemantics]Definition Index
A
active [in CBPV.StrongNormalisation]activev [in CBPV.StrongNormalisation]
ap [in CBPV.fintype]
apc [in CBPV.fintype]
B
Bool [in CBPV.CBN.DenotationalSemantics]Bool [in CBPV.CBV.DenotationalSemantics]
bound [in CBPV.fintype]
C
C [in CBPV.LogicalEquivalence]C [in CBPV.SemanticTyping]
C [in CBPV.StrongNormalisation]
caseScott [in CBPV.CBN.DenotationalSemantics]
cbn_typepres_substitution [in CBPV.CBN.CBN_CBPV]
cbn_typepres_renaming [in CBPV.CBN.CBN_CBPV]
cbn_ctx [in CBPV.CBN.CBN_CBPV]
CCBPVc [in CBPV.DenotationalSemantics]
CCBPVv [in CBPV.DenotationalSemantics]
cctx_comp_typing_soundness [in CBPV.ProgramContexts]
cctx_value_typing_soundness [in CBPV.ProgramContexts]
cctx_cctx_plug_typing_soundness [in CBPV.ProgramContexts]
cctx_vctx_plug_typing_soundness [in CBPV.ProgramContexts]
cctx_typing_ind_3 [in CBPV.ProgramContexts]
cctx_typing_ind_2 [in CBPV.ProgramContexts]
cctx_ind_2 [in CBPV.ProgramContexts]
cctxᵥ_cctx_comp [in CBPV.CBV.DenotationalSemantics]
cctxᵥ_cctx_value [in CBPV.CBV.DenotationalSemantics]
cctxᵥ_comp_typing_soundness [in CBPV.CBV.DenotationalSemantics]
cctxᵥ_value_typing_soundness [in CBPV.CBV.DenotationalSemantics]
cctxᵥ_typing_ind_3 [in CBPV.CBV.DenotationalSemantics]
cctxᵥ_typing_ind_2 [in CBPV.CBV.DenotationalSemantics]
cctxᵥ_ind_2 [in CBPV.CBV.DenotationalSemantics]
comp [in CBPV.fintype]
compRenRen_comp [in CBPV.Syntax]
compRenRen_value [in CBPV.Syntax]
compRenRen_exp [in CBPV.CBN.CBN]
compRenRen_Exp [in CBPV.CBV.CBV]
compRenRen_Value [in CBPV.CBV.CBV]
compRenSubst_comp [in CBPV.Syntax]
compRenSubst_value [in CBPV.Syntax]
compRenSubst_exp [in CBPV.CBN.CBN]
compRenSubst_Exp [in CBPV.CBV.CBV]
compRenSubst_Value [in CBPV.CBV.CBV]
compSubstRen__comp [in CBPV.Syntax]
compSubstRen__value [in CBPV.Syntax]
compSubstRen__exp [in CBPV.CBN.CBN]
compSubstRen__Exp [in CBPV.CBV.CBV]
compSubstRen__Value [in CBPV.CBV.CBV]
compSubstSubst_comp [in CBPV.Syntax]
compSubstSubst_value [in CBPV.Syntax]
compSubstSubst_exp [in CBPV.CBN.CBN]
compSubstSubst_Exp [in CBPV.CBV.CBV]
compSubstSubst_Value [in CBPV.CBV.CBV]
comptypeif [in CBPV.ProgramContexts]
comptype_ind_2 [in CBPV.Terms]
computation_typing_ind_4 [in CBPV.SyntacticTyping]
computation_typing_ind_3 [in CBPV.SyntacticTyping]
computation_typing_ind_2 [in CBPV.SyntacticTyping]
comp_semeq [in CBPV.LogicalEquivalence]
comp_semtype [in CBPV.SemanticTyping]
comp_typepres_substitution [in CBPV.SyntacticTyping]
comp_typepres_renaming [in CBPV.SyntacticTyping]
comp_semtype [in CBPV.StrongNormalisation]
comp_ind_2 [in CBPV.Terms]
comp_obseq [in CBPV.ObservationalEquivalence]
confluent [in CBPV.AbstractReductionSystems]
context_typing_decomposition_cctx_comp [in CBPV.ProgramContexts]
context_typing_decomposition_cctx_value [in CBPV.ProgramContexts]
context_typing_decomposition_vctx_comp [in CBPV.ProgramContexts]
context_typing_decomposition_vctx_value [in CBPV.ProgramContexts]
ctx [in CBPV.SyntacticTyping]
ctx_cbv [in CBPV.CBV.CBV_CBPV]
D
denote_comptyping [in CBPV.DenotationalSemantics]denote_valtyping [in CBPV.DenotationalSemantics]
denote_context [in CBPV.DenotationalSemantics]
denote_comptype [in CBPV.DenotationalSemantics]
denote_valtype [in CBPV.DenotationalSemantics]
denote_cbn_ctx [in CBPV.CBN.DenotationalSemantics]
denote_exp [in CBPV.CBN.DenotationalSemantics]
denote_type [in CBPV.CBN.DenotationalSemantics]
denote_cbv_ctx [in CBPV.CBV.DenotationalSemantics]
denote_val [in CBPV.CBV.DenotationalSemantics]
denote_exp [in CBPV.CBV.DenotationalSemantics]
denote_type [in CBPV.CBV.DenotationalSemantics]
diamond [in CBPV.AbstractReductionSystems]
E
eagerlet [in CBPV.Eagerlet]ectx_typing_soundness [in CBPV.CBN.DenotationalSemantics]
Equiv [in CBPV.EquationalTheory]
equiv [in CBPV.AbstractReductionSystems]
EquivCBN [in CBPV.EquationalTheory]
EquivCBV [in CBPV.EquationalTheory]
EquivCBVᵥ [in CBPV.EquationalTheory]
Equivᵥ [in CBPV.EquationalTheory]
eta_if' [in CBPV.CBN.DenotationalSemantics]
eta_if [in CBPV.CBN.DenotationalSemantics]
eval [in CBPV.Semantics]
eval [in CBPV.CBN.CBN_CBPV]
evaluates [in CBPV.AbstractReductionSystems]
eval_exp [in CBPV.CBV.CBV_CBPV]
eval_val [in CBPV.CBV.CBV_CBPV]
eval_ty [in CBPV.CBV.CBV_CBPV]
eval_CBN [in CBPV.CBN.DenotationalSemantics]
eval_ectx [in CBPV.CBN.DenotationalSemantics]
eval_subst [in CBPV.CBN.CBN_CBPV]
eval_ctx [in CBPV.CBN.CBN_CBPV]
eval_ty [in CBPV.CBN.CBN_CBPV]
eval_CBVᵥ [in CBPV.CBV.DenotationalSemantics]
eval_CBV [in CBPV.CBV.DenotationalSemantics]
eval' [in CBPV.CBN.DenotationalSemantics]
eval'_vctx_comp_typing [in CBPV.CBV.DenotationalSemantics]
eval'_vctx_value_typing [in CBPV.CBV.DenotationalSemantics]
eval'_cctx_comp_typing [in CBPV.CBV.DenotationalSemantics]
eval'_cctx_value_typing [in CBPV.CBV.DenotationalSemantics]
eval'_cctx [in CBPV.CBV.DenotationalSemantics]
eval'_vctx [in CBPV.CBV.DenotationalSemantics]
eval'_exp [in CBPV.CBV.DenotationalSemantics]
eval'_val [in CBPV.CBV.DenotationalSemantics]
exponential_t_algebra [in CBPV.DenotationalSemantics]
ExpVal_ind [in CBPV.CBV.CBV_CBPV]
Exp_ind_2 [in CBPV.CBV.CBV_CBPV]
exp_obseq [in CBPV.CBN.DenotationalSemantics]
exp_value_ind_2 [in CBPV.CBV.strongStory]
exp_obseq [in CBPV.CBV.DenotationalSemantics]
extend [in CBPV.DenotationalSemantics]
extend' [in CBPV.DenotationalSemantics]
extRen_comp [in CBPV.Syntax]
extRen_value [in CBPV.Syntax]
extRen_exp [in CBPV.CBN.CBN]
extRen_Exp [in CBPV.CBV.CBV]
extRen_Value [in CBPV.CBV.CBV]
ext_comp [in CBPV.Syntax]
ext_value [in CBPV.Syntax]
ext_exp [in CBPV.CBN.CBN]
ext_Exp [in CBPV.CBV.CBV]
ext_Value [in CBPV.CBV.CBV]
E' [in CBPV.LogicalEquivalence]
E' [in CBPV.SemanticTyping]
F
ff [in CBPV.CBN.DenotationalSemantics]ff [in CBPV.CBV.DenotationalSemantics]
fill [in CBPV.Semantics]
fillc [in CBPV.ProgramContexts]
fillcᵥ [in CBPV.CBV.DenotationalSemantics]
fille [in CBPV.CBN.DenotationalSemantics]
fillv [in CBPV.ProgramContexts]
fillvᵥ [in CBPV.CBV.DenotationalSemantics]
fin [in CBPV.fintype]
fmap [in CBPV.DenotationalSemantics]
free_t_algebra [in CBPV.DenotationalSemantics]
funcomp [in CBPV.fintype]
functional [in CBPV.AbstractReductionSystems]
G
G [in CBPV.LogicalEquivalence]G [in CBPV.SemanticTyping]
G [in CBPV.StrongNormalisation]
gbool [in CBPV.CBN.DenotationalSemantics]
gbool [in CBPV.CBV.DenotationalSemantics]
H
has_type_ind [in CBPV.CBV.DenotationalSemantics]has_typeE_2 [in CBPV.CBV.DenotationalSemantics]
has_typeV_2 [in CBPV.CBV.DenotationalSemantics]
I
id [in CBPV.fintype]IdMonad [in CBPV.DenotationalSemantics]
idren [in CBPV.fintype]
idSubst_comp [in CBPV.Syntax]
idSubst_value [in CBPV.Syntax]
idSubst_exp [in CBPV.CBN.CBN]
idSubst_Exp [in CBPV.CBV.CBV]
idSubst_Value [in CBPV.CBV.CBV]
it [in CBPV.Base]
J
joinable [in CBPV.AbstractReductionSystems]K
K [in CBPV.CBN.DenotationalSemantics]M
morphism [in CBPV.AbstractReductionSystems]mu [in CBPV.DenotationalSemantics]
mutindt_vctx_cctx_typing [in CBPV.ProgramContexts]
mutindt_value_computation_typing [in CBPV.SyntacticTyping]
mutindt_vctxᵥ_cctxᵥ_typing [in CBPV.CBV.DenotationalSemantics]
mutind_vctx_cctx_typing [in CBPV.ProgramContexts]
mutind_vctx_cctx [in CBPV.ProgramContexts]
mutind_value_computation_typing [in CBPV.SyntacticTyping]
mutind_value_exp [in CBPV.CBV.strongStory]
mutind_valtype_comptype [in CBPV.Terms]
mutind_val_comp [in CBPV.Terms]
mutind_parstep [in CBPV.Confluence]
mutind_vctxᵥ_cctxᵥ_typing [in CBPV.CBV.DenotationalSemantics]
mutind_cbv_ctx [in CBPV.CBV.DenotationalSemantics]
mutind_sstep [in CBPV.StrongReduction]
N
nat_to_fin [in CBPV.Terms]Normal [in CBPV.AbstractReductionSystems]
null [in CBPV.fintype]
O
one [in CBPV.EquationalTheory]P
parstepc_subst [in CBPV.Confluence]parstepc_renaming [in CBPV.Confluence]
parstepc_ind_2 [in CBPV.Confluence]
parstepv_subst [in CBPV.Confluence]
parstepv_renaming [in CBPV.Confluence]
parstepv_ind_2 [in CBPV.Confluence]
plugcctx [in CBPV.ProgramContexts]
plugvctx [in CBPV.ProgramContexts]
plug_fill_cctx_comp [in CBPV.ProgramContexts]
plug_fill_cctx_value [in CBPV.ProgramContexts]
plug_fill_vctx_comp [in CBPV.ProgramContexts]
plug_fill_vctx_value [in CBPV.ProgramContexts]
primitive_step_subst_value [in CBPV.StrongReduction]
primitive_step_subst [in CBPV.StrongReduction]
product_t_algebra [in CBPV.DenotationalSemantics]
R
RC [in CBPV.DenotationalSemantics]ren [in CBPV.fintype]
ren_comp [in CBPV.Syntax]
ren_value [in CBPV.Syntax]
ren_exp [in CBPV.CBN.CBN]
ren_Exp [in CBPV.CBV.CBV]
ren_Value [in CBPV.CBV.CBV]
rho [in CBPV.Confluence]
rhoᵥ [in CBPV.Confluence]
rinstInst_up_value_value [in CBPV.Syntax]
rinstInst_up_exp_exp [in CBPV.CBN.CBN]
rinstInst_up_Value_Value [in CBPV.CBV.CBV]
rinst_inst_comp [in CBPV.Syntax]
rinst_inst_value [in CBPV.Syntax]
rinst_inst_exp [in CBPV.CBN.CBN]
rinst_inst_Exp [in CBPV.CBV.CBV]
rinst_inst_Value [in CBPV.CBV.CBV]
RV [in CBPV.DenotationalSemantics]
S
scons [in CBPV.fintype]semi_confluent [in CBPV.AbstractReductionSystems]
shift [in CBPV.fintype]
singleton_t_algebra [in CBPV.DenotationalSemantics]
sn [in CBPV.StrongReduction]
snv [in CBPV.StrongReduction]
sstep_value_parstepv [in CBPV.Confluence]
sstep_parstepc [in CBPV.Confluence]
sstep_value_anti_renaming [in CBPV.StrongReduction]
sstep_anti_renaming [in CBPV.StrongReduction]
sstep_value_lemma [in CBPV.StrongReduction]
sstep_lemma [in CBPV.StrongReduction]
sstep_value_congruence_value [in CBPV.StrongReduction]
sstep_value_congruence [in CBPV.StrongReduction]
sstep_congruence_value [in CBPV.StrongReduction]
sstep_congruence [in CBPV.StrongReduction]
sstep_ind_2 [in CBPV.StrongReduction]
sstep_value_ind_2 [in CBPV.StrongReduction]
StepVal_preserved [in CBPV.CBV.strongStory]
Step_preserved [in CBPV.CBV.strongStory]
sub [in CBPV.EquationalTheory]
subst_comp [in CBPV.Syntax]
subst_value [in CBPV.Syntax]
subst_exp [in CBPV.CBN.CBN]
subst_Exp [in CBPV.CBV.CBV]
subst_Value [in CBPV.CBV.CBV]
sub₂ [in CBPV.EquationalTheory]
swap [in CBPV.EquationalTheory]
T
tak_fun [in CBPV.TMT]to_valtype [in CBPV.Terms]
tt [in CBPV.CBN.DenotationalSemantics]
tt [in CBPV.CBV.DenotationalSemantics]
typingExp_pres [in CBPV.CBV.CBV_CBPV]
typingExp_pres' [in CBPV.CBV.DenotationalSemantics]
typingVal_pres [in CBPV.CBV.CBV_CBPV]
typingVal_pres' [in CBPV.CBV.DenotationalSemantics]
U
upExtRen_value_value [in CBPV.Syntax]upExtRen_exp_exp [in CBPV.CBN.CBN]
upExtRen_Value_Value [in CBPV.CBV.CBV]
upExt_value_value [in CBPV.Syntax]
upExt_exp_exp [in CBPV.CBN.CBN]
upExt_Value_Value [in CBPV.CBV.CBV]
upId_value_value [in CBPV.Syntax]
upId_exp_exp [in CBPV.CBN.CBN]
upId_Value_Value [in CBPV.CBV.CBV]
upRen_value_value [in CBPV.Syntax]
upRen_exp_exp [in CBPV.CBN.CBN]
upRen_Value_Value [in CBPV.CBV.CBV]
up_subst_subst_value_value [in CBPV.Syntax]
up_subst_ren_value_value [in CBPV.Syntax]
up_ren_subst_value_value [in CBPV.Syntax]
up_value_value [in CBPV.Syntax]
up_ren [in CBPV.fintype]
up_subst_subst_exp_exp [in CBPV.CBN.CBN]
up_subst_ren_exp_exp [in CBPV.CBN.CBN]
up_ren_subst_exp_exp [in CBPV.CBN.CBN]
up_exp_exp [in CBPV.CBN.CBN]
up_subst_subst_Value_Value [in CBPV.CBV.CBV]
up_subst_ren_Value_Value [in CBPV.CBV.CBV]
up_ren_subst_Value_Value [in CBPV.CBV.CBV]
up_Value_Value [in CBPV.CBV.CBV]
V
V [in CBPV.LogicalEquivalence]V [in CBPV.SemanticTyping]
V [in CBPV.StrongNormalisation]
valtypeif [in CBPV.ProgramContexts]
valtype_ind_2 [in CBPV.Terms]
Value_ind_2 [in CBPV.CBV.CBV_CBPV]
value_typepres_substitution [in CBPV.SyntacticTyping]
value_typepres_renaming [in CBPV.SyntacticTyping]
value_typing_ind_4 [in CBPV.SyntacticTyping]
value_typing_ind_3 [in CBPV.SyntacticTyping]
value_typing_ind_2 [in CBPV.SyntacticTyping]
value_exp_ind_2 [in CBPV.CBV.strongStory]
value_ind_2 [in CBPV.Terms]
value_obseq [in CBPV.ObservationalEquivalence]
value_obseq [in CBPV.CBV.DenotationalSemantics]
val_semeq [in CBPV.LogicalEquivalence]
val_semtype [in CBPV.SemanticTyping]
val_semtype [in CBPV.StrongNormalisation]
var [in CBPV.Terms]
var_zero [in CBPV.fintype]
vctx_comp_typing_soundness [in CBPV.ProgramContexts]
vctx_value_typing_soundness [in CBPV.ProgramContexts]
vctx_cctx_plug_typing_soundness [in CBPV.ProgramContexts]
vctx_vctx_plug_typing_soundness [in CBPV.ProgramContexts]
vctx_typing_ind_3 [in CBPV.ProgramContexts]
vctx_typing_ind_2 [in CBPV.ProgramContexts]
vctx_ind_2 [in CBPV.ProgramContexts]
vctxᵥ_vctx_comp [in CBPV.CBV.DenotationalSemantics]
vctxᵥ_vctx_value [in CBPV.CBV.DenotationalSemantics]
vctxᵥ_comp_typing_soundness [in CBPV.CBV.DenotationalSemantics]
vctxᵥ_value_typing_soundness [in CBPV.CBV.DenotationalSemantics]
vctxᵥ_typing_ind_3 [in CBPV.CBV.DenotationalSemantics]
vctxᵥ_typing_ind_2 [in CBPV.CBV.DenotationalSemantics]
vctxᵥ_ind_2 [in CBPV.CBV.DenotationalSemantics]
Z
zero [in CBPV.EquationalTheory]Record Index
C
CBN [in CBPV.CBN.DenotationalSemantics]CBPVc [in CBPV.ObservationalEquivalence]
CBPVv [in CBPV.ObservationalEquivalence]
CBV [in CBPV.CBV.DenotationalSemantics]
CBVᵥ [in CBPV.CBV.DenotationalSemantics]
M
Monad [in CBPV.DenotationalSemantics]P
ParallelReduction [in CBPV.Confluence]R
Ren1 [in CBPV.fintype]Ren2 [in CBPV.fintype]
S
Subst1 [in CBPV.fintype]Subst2 [in CBPV.fintype]
T
TAlgebra [in CBPV.DenotationalSemantics]V
Var [in CBPV.fintype]| 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 | (1624 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 | (78 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 | (2 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 | (77 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 | (30 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 | (524 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 | (348 entries) |
| Axiom 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) |
| 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 | (60 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 | (26 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (123 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 | (18 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 | (9 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (315 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 | (13 entries) |