| 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 | (2105 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 | (62 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 | (12 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 | (238 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 | (63 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 | (881 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 | (172 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 | (10 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (43 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 | (57 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 | (113 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 | (68 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 | (40 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 | (316 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 | (30 entries) |
Global Index
A
abstract [library]AbstractPredTrans [section, in semantics.wp.abstract]
AbstractPredTrans.E [variable, in semantics.wp.abstract]
AbstractPredTrans.T [variable, in semantics.wp.abstract]
AbstractPredTrans.X [variable, in semantics.wp.abstract]
AbstractPredTrans.Y [variable, in semantics.wp.abstract]
accn [inductive, in semantics.ars]
accnH [constructor, in semantics.ars]
accnL [constructor, in semantics.ars]
accn_inv [lemma, in semantics.ars]
accn_ind' [definition, in semantics.ars]
accumulate [lemma, in semantics.tower.parameterized]
acc_on_i [constructor, in semantics.tower.linear_tower]
acc_on [inductive, in semantics.tower.linear_tower]
Act [constructor, in semantics.wp.ic]
Act [constructor, in semantics.ccs.syntax]
act [inductive, in semantics.ccs.syntax]
action [axiom, in semantics.wp.states]
actionE [axiom, in semantics.wp.states]
action_eqP [axiom, in semantics.wp.states]
action_eq [axiom, in semantics.wp.states]
active [definition, in semantics.f.strongnorm]
ActRecv [constructor, in semantics.ccs.syntax]
ActSend [constructor, in semantics.ccs.syntax]
ActTau [constructor, in semantics.ccs.syntax]
act_proper_l [instance, in semantics.ccs.bisim]
act_proper [instance, in semantics.ccs.bisim]
adj [library]
adjA [lemma, in semantics.ord.adj]
adjAc [lemma, in semantics.ord.adj]
adjB [lemma, in semantics.ord.adj]
adjE [lemma, in semantics.ord.adj]
adjEc [lemma, in semantics.ord.adj]
adjH [lemma, in semantics.ord.adj]
adjJ [lemma, in semantics.ord.adj]
adjM [lemma, in semantics.ord.adj]
adjP [lemma, in semantics.ord.adj]
adjT [lemma, in semantics.ord.adj]
AdjunctionsCLat [section, in semantics.ord.adj]
AdjunctionsCLat.f [variable, in semantics.ord.adj]
AdjunctionsCLat.g [variable, in semantics.ord.adj]
AdjunctionsCLat.X [variable, in semantics.ord.adj]
AdjunctionsCLat.Y [variable, in semantics.ord.adj]
AdjunctionsFrame [section, in semantics.ord.adj]
AdjunctionsFrame.f [variable, in semantics.ord.adj]
AdjunctionsFrame.g [variable, in semantics.ord.adj]
AdjunctionsFrame.X [variable, in semantics.ord.adj]
AdjunctionsFrame.Y [variable, in semantics.ord.adj]
AdjunctionsOrd [section, in semantics.ord.adj]
AdjunctionsOrdDual [section, in semantics.ord.adj]
AdjunctionsOrdDual.X [variable, in semantics.ord.adj]
AdjunctionsOrdDual.Xr [variable, in semantics.ord.adj]
AdjunctionsOrdDual.Y [variable, in semantics.ord.adj]
AdjunctionsOrdDual.Yr [variable, in semantics.ord.adj]
AdjunctionsOrd.X [variable, in semantics.ord.adj]
AdjunctionsOrd.Y [variable, in semantics.ord.adj]
adj_tripleR [lemma, in semantics.ord.adj]
adj_uniqL [lemma, in semantics.ord.adj]
adj_tripleL [lemma, in semantics.ord.adj]
adj_uniqR [lemma, in semantics.ord.adj]
adj_glb [lemma, in semantics.ord.adj]
adj_monoR [instance, in semantics.ord.adj]
adj_counit [lemma, in semantics.ord.adj]
adj_lub [lemma, in semantics.ord.adj]
adj_monoL [instance, in semantics.ord.adj]
adj_unit [lemma, in semantics.ord.adj]
All [projection, in semantics.f.types]
all [constructor, in semantics.f.types]
allc_sigma [lemma, in semantics.tower.cocontinuous_tower]
allE [lemma, in semantics.ord.clat]
allEc [lemma, in semantics.ord.clat]
allI [lemma, in semantics.ord.clat]
allIc [lemma, in semantics.ord.clat]
all_def [lemma, in semantics.ord.clat]
all_mono [lemma, in semantics.ord.clat]
all_axiom [lemma, in semantics.ord.clat]
all2 [definition, in semantics.wp.gc]
all2P [lemma, in semantics.wp.gc]
antisymmetric [definition, in semantics.base.overture]
ap [definition, in semantics.base.overture]
app [constructor, in semantics.f.fsyntax]
app [constructor, in semantics.debruijn.syntax]
app [constructor, in semantics.ccomega.syntax]
app [constructor, in semantics.f.fcbvsyntax]
Arr [projection, in semantics.f.types]
arr [constructor, in semantics.f.types]
ars [library]
asimpl [definition, in semantics.ccs.syntax]
Assn [constructor, in semantics.wp.gc]
AssociatedClosure [section, in semantics.tower.associated_closure]
AssociatedClosure.ic [variable, in semantics.tower.associated_closure]
associated_closure [library]
B
base [library]basis [definition, in semantics.ord.sheaf]
basisE [lemma, in semantics.ord.sheaf]
BasisLaws [section, in semantics.ord.sheaf]
BasisLaws.cov [variable, in semantics.ord.sheaf]
BasisLaws.X [variable, in semantics.ord.sheaf]
basisP [lemma, in semantics.ord.sheaf]
basis_cov [projection, in semantics.ord.sheaf]
basis_pred [record, in semantics.ord.sheaf]
below_companion_sound [lemma, in semantics.tower.parameterized]
below_companion_to_upto [lemma, in semantics.tower.tower]
bijective_equiv [definition, in semantics.base.inhab]
bisim [abbreviation, in semantics.ccs.bisim]
Bisim [abbreviation, in semantics.ccs.bisim]
bisim [definition, in semantics.tower.ex_streams]
bisim [library]
bisim_equiv [instance, in semantics.ccs.bisim]
bisim_rewrite [instance, in semantics.ccs.bisim]
bisim_left [lemma, in semantics.ccs.bisim]
bisim_bisim [lemma, in semantics.ccs.bisim]
bisim_unfold [lemma, in semantics.ccs.bisim]
bisim_fold [lemma, in semantics.ccs.bisim]
Bisim_mono [instance, in semantics.ccs.bisim]
bisim_coind [lemma, in semantics.ccs.bisim]
bisim_eq [lemma, in semantics.tower.ex_streams]
bisim_def [lemma, in semantics.tower.ex_streams]
bot [definition, in semantics.ord.clat]
botE [lemma, in semantics.ord.clat]
bot_def [lemma, in semantics.ord.clat]
bot_eq [lemma, in semantics.ord.clat]
bound [definition, in semantics.data.fintype]
C
C [definition, in semantics.f.strongnorm]C [inductive, in semantics.ccs.properties]
C [inductive, in semantics.tower.direct_induction]
canonical [definition, in semantics.ord.sheaf]
CanonicalBasis [section, in semantics.ord.sheaf]
CanonicalBasis.X [variable, in semantics.ord.sheaf]
CanonicalCoverage [section, in semantics.ord.sheaf]
CanonicalCoverage.X [variable, in semantics.ord.sheaf]
canonicalE [lemma, in semantics.ord.sheaf]
canonicalP [lemma, in semantics.ord.sheaf]
canonical_sup [lemma, in semantics.ord.sheaf]
canonical_is_subcanonical [instance, in semantics.ord.sheaf]
Case [constructor, in semantics.wp.gc]
CcsCongruence [record, in semantics.ccs.bisim]
ccs_congruence_bisim [instance, in semantics.ccs.bisim]
ccs_congruence_fix [projection, in semantics.ccs.bisim]
ccs_congruence_new [projection, in semantics.ccs.bisim]
ccs_congruence_par [projection, in semantics.ccs.bisim]
ccs_congruence_sum [projection, in semantics.ccs.bisim]
cempty [definition, in semantics.ccomega.subjectreduction]
cexp [definition, in semantics.ccs.semantics]
chain [definition, in semantics.tower.cocontinuous_tower]
chain_dec [lemma, in semantics.tower.cocontinuous_tower]
Characterization [section, in semantics.tower.associated_closure]
Characterization.A [variable, in semantics.tower.associated_closure]
Characterization.closure_operatorT [variable, in semantics.tower.associated_closure]
Characterization.inf_closedT [variable, in semantics.tower.associated_closure]
Chu [section, in semantics.tower.llat]
chuL [projection, in semantics.tower.llat]
chuP [lemma, in semantics.tower.llat]
chuR [projection, in semantics.tower.llat]
churchrosser [library]
church_rosser [lemma, in semantics.ccomega.churchrosser]
chu_lt_inf [lemma, in semantics.tower.llat]
chu_lt_right [lemma, in semantics.tower.llat]
chu_lt_left [lemma, in semantics.tower.llat]
chu_lt [definition, in semantics.tower.llat]
chu_infP [lemma, in semantics.tower.llat]
chu_inf [definition, in semantics.tower.llat]
chu_le_eq [lemma, in semantics.tower.llat]
chu_eq [lemma, in semantics.tower.llat]
chu_le_trans [lemma, in semantics.tower.llat]
chu_le_refl [lemma, in semantics.tower.llat]
chu_le [definition, in semantics.tower.llat]
classic [definition, in semantics.tower.linear_tower]
ClassicalTower [section, in semantics.tower.linear_tower]
ClassicalTower.f [variable, in semantics.tower.linear_tower]
ClassicalTower.f_mono [variable, in semantics.tower.linear_tower]
ClassicalTower.X [variable, in semantics.tower.linear_tower]
ClassicalTower.xm [variable, in semantics.tower.linear_tower]
classical_tower_max [lemma, in semantics.tower.linear_tower]
classical_tower_linear [lemma, in semantics.tower.linear_tower]
classical_tower_glue [lemma, in semantics.tower.linear_tower]
classical_lt_inf [lemma, in semantics.tower.linear_tower]
classical_lt_right [lemma, in semantics.tower.linear_tower]
classical_lt_left [lemma, in semantics.tower.linear_tower]
classical_lt [definition, in semantics.tower.linear_tower]
classic_mono_to_lmono [lemma, in semantics.tower.linear_tower]
CLat [module, in semantics.ord.clat]
clat [library]
CLatDef [section, in semantics.ord.clat]
CLatDef.T [variable, in semantics.ord.clat]
CLatLaws [section, in semantics.ord.clat]
CLatLaws.T [variable, in semantics.ord.clat]
CLat.base [projection, in semantics.ord.clat]
CLat.class [definition, in semantics.ord.clat]
CLat.Class [constructor, in semantics.ord.clat]
CLat.ClassDef [section, in semantics.ord.clat]
CLat.ClassDef.cT [variable, in semantics.ord.clat]
CLat.ClassDef.T [variable, in semantics.ord.clat]
CLat.ClassDef.xT [variable, in semantics.ord.clat]
CLat.class_of [record, in semantics.ord.clat]
CLat.clone [definition, in semantics.ord.clat]
CLat.Exports [module, in semantics.ord.clat]
CLat.Exports.CLat [abbreviation, in semantics.ord.clat]
CLat.Exports.clat [abbreviation, in semantics.ord.clat]
CLat.Exports.CLatMixin [abbreviation, in semantics.ord.clat]
[ clat of _ ] (form_scope) [notation, in semantics.ord.clat]
[ clat of _ for _ ] (form_scope) [notation, in semantics.ord.clat]
[ clatMixin of _ ] (form_scope) [notation, in semantics.ord.clat]
CLat.inf [projection, in semantics.ord.clat]
CLat.mixin [projection, in semantics.ord.clat]
CLat.Mixin [constructor, in semantics.ord.clat]
CLat.mixin_of [record, in semantics.ord.clat]
CLat.ordType [definition, in semantics.ord.clat]
CLat.pack [definition, in semantics.ord.clat]
CLat.Pack [constructor, in semantics.ord.clat]
CLat.proType [definition, in semantics.ord.clat]
CLat.sort [projection, in semantics.ord.clat]
CLat.type [record, in semantics.ord.clat]
CLat.xclass [abbreviation, in semantics.ord.clat]
closureA [lemma, in semantics.ord.adj]
closureAc [lemma, in semantics.ord.adj]
ClosureCLat [section, in semantics.ord.adj]
closureE [lemma, in semantics.ord.adj]
closureEc [lemma, in semantics.ord.adj]
closureJ [lemma, in semantics.ord.adj]
closureM [lemma, in semantics.ord.adj]
ClosureOperatorsOrdType [section, in semantics.ord.adj]
ClosureOperatorsProType [section, in semantics.ord.adj]
closureP [lemma, in semantics.ord.adj]
closureT [lemma, in semantics.ord.adj]
closure_inf_closed [lemma, in semantics.tower.associated_closure]
closure_to_inf_closed_retr [lemma, in semantics.tower.associated_closure]
closure_to_inf_closed [definition, in semantics.tower.associated_closure]
closure_of_image [lemma, in semantics.tower.associated_closure]
closure_of_is_closure [instance, in semantics.tower.associated_closure]
closure_of_stable [lemma, in semantics.tower.associated_closure]
closure_of [definition, in semantics.tower.associated_closure]
closure_glb [lemma, in semantics.ord.adj]
closure_lub [lemma, in semantics.ord.adj]
closure_stable [lemma, in semantics.ord.adj]
closure_eq [lemma, in semantics.ord.adj]
closure_idem [lemma, in semantics.ord.adj]
closure_inc [lemma, in semantics.ord.adj]
cmd [inductive, in semantics.wp.gc]
CmdEqType [section, in semantics.wp.gc]
CmdInduction [section, in semantics.wp.gc]
CmdInduction.P [variable, in semantics.wp.gc]
CmdInduction.p_do [variable, in semantics.wp.gc]
CmdInduction.p_case [variable, in semantics.wp.gc]
CmdInduction.p_seq [variable, in semantics.wp.gc]
CmdInduction.p_assn [variable, in semantics.wp.gc]
CmdInduction.p_skip [variable, in semantics.wp.gc]
cmd_ind [lemma, in semantics.wp.gc]
cmd_eqP [lemma, in semantics.wp.gc]
cmd_eq [definition, in semantics.wp.gc]
cmd_ind' [definition, in semantics.wp.gc]
cmorph [definition, in semantics.ccomega.contextmorphism]
co [definition, in semantics.tower.gfp_companion]
cocontinuous_tower [library]
codirected [definition, in semantics.tower.cocontinuous_tower]
codirected [definition, in semantics.tower.direct_induction]
coE [lemma, in semantics.tower.gfp_companion]
cofinal [definition, in semantics.ars]
CoFinal [section, in semantics.ars]
cofinal_normalizing [lemma, in semantics.ars]
CoFinal.e [variable, in semantics.ars]
CoFinal.rho [variable, in semantics.ars]
CoFinal.T [variable, in semantics.ars]
CoFinal.tri [variable, in semantics.ars]
com [definition, in semantics.ars]
Commutation [section, in semantics.ars]
Commutation.T [variable, in semantics.ars]
comp [definition, in semantics.wp.compiler]
companion_coind [lemma, in semantics.tower.parameterized]
companion_co [lemma, in semantics.tower.gfp_companion]
compatible [definition, in semantics.tower.tower]
compile [abbreviation, in semantics.wp.compiler]
compiler [library]
CompilerCorrectness [section, in semantics.wp.compiler]
CompilerCorrectness.Flatten [section, in semantics.wp.compiler]
ComputationN [section, in semantics.ars]
ComputationN.classical [variable, in semantics.ars]
ComputationN.e [variable, in semantics.ars]
ComputationN.norm [variable, in semantics.ars]
ComputationN.rho [variable, in semantics.ars]
ComputationN.sound [variable, in semantics.ars]
ComputationN.T [variable, in semantics.ars]
com_lift [lemma, in semantics.ars]
com_strip [lemma, in semantics.ars]
conf [definition, in semantics.wp.icsemantics]
confluent [definition, in semantics.ars]
confluent_cr [lemma, in semantics.ars]
CongruenceProofs [section, in semantics.ccs.bisim]
CongruenceProofs.congruence_properties [variable, in semantics.ccs.bisim]
CongruenceProofs.R [variable, in semantics.ccs.bisim]
congruence_step [lemma, in semantics.ccs.bisim]
constant [definition, in semantics.base.fext]
cont [library]
contB [lemma, in semantics.ord.cont]
ContCLat [section, in semantics.ord.cont]
contE [lemma, in semantics.ord.cont]
contEc [lemma, in semantics.ord.cont]
contextmorphism [library]
context_ok [definition, in semantics.ccomega.typing]
context_ok_ext [lemma, in semantics.ccomega.subjectreduction]
ContFrame [section, in semantics.ord.cont]
ContFrame.is_embedding [variable, in semantics.ord.cont]
contH [lemma, in semantics.ord.cont]
continuous [definition, in semantics.wp.abstract]
continuous [definition, in semantics.wp.gcsemantics]
ContinuousSup [section, in semantics.wp.prelim]
ContinuousSup.dF [variable, in semantics.wp.prelim]
ContinuousSup.F [variable, in semantics.wp.prelim]
ContinuousSup.I [variable, in semantics.wp.prelim]
ContinuousSup.J [variable, in semantics.wp.prelim]
ContinuousSup.j0 [variable, in semantics.wp.prelim]
ContinuousSup.X [variable, in semantics.wp.prelim]
continuous_directed_meet_sup [lemma, in semantics.wp.prelim]
continuous_directed_meet_sup [lemma, in semantics.wp.abstract]
contJ [lemma, in semantics.ord.cont]
contM [projection, in semantics.ord.cont]
contT [projection, in semantics.ord.cont]
cont_embH [lemma, in semantics.ord.cont]
cont_is_adjunction_frame [instance, in semantics.ord.cont]
cont_is_adjunction [projection, in semantics.ord.cont]
conv [inductive, in semantics.ars]
conv [inductive, in semantics.base.quotient]
convES [lemma, in semantics.ars]
convESi [lemma, in semantics.ars]
convR [constructor, in semantics.ars]
convSE [constructor, in semantics.ars]
convSEi [constructor, in semantics.ars]
convxx [constructor, in semantics.base.quotient]
conv_closure [lemma, in semantics.ars]
conv_hom [lemma, in semantics.ars]
conv_img [lemma, in semantics.ars]
conv_sym [lemma, in semantics.ars]
conv_trans [lemma, in semantics.ars]
conv_beta [lemma, in semantics.ccomega.reduction]
conv_compat [lemma, in semantics.ccomega.reduction]
conv_subst [lemma, in semantics.ccomega.reduction]
conv_prod [lemma, in semantics.ccomega.reduction]
conv_lam [lemma, in semantics.ccomega.reduction]
conv_app [lemma, in semantics.ccomega.reduction]
conv_sub [lemma, in semantics.ccomega.subtyping]
conv_sub1 [lemma, in semantics.ccomega.subtyping]
conv_prod_sort [lemma, in semantics.ccomega.churchrosser]
conv_equiv [lemma, in semantics.base.quotient]
conv_repr [lemma, in semantics.base.quotient]
conv1 [lemma, in semantics.ars]
conv1i [lemma, in semantics.ars]
conv1R [constructor, in semantics.base.quotient]
conv1S [constructor, in semantics.base.quotient]
countable_branching [definition, in semantics.tower.ex_similarity]
Cover [definition, in semantics.ord.sheaf]
Coverage [section, in semantics.ord.sheaf]
coverage [inductive, in semantics.ord.sheaf]
coverageP [lemma, in semantics.ord.sheaf]
coverage_sheafify_adj [lemma, in semantics.ord.sheaf]
coverage_sheafify_inc [lemma, in semantics.ord.sheaf]
coverage_sheafify [definition, in semantics.ord.sheaf]
coverage_trans [lemma, in semantics.ord.sheaf]
cover_cover [constructor, in semantics.ord.sheaf]
cover_max [constructor, in semantics.ord.sheaf]
cover_sup [lemma, in semantics.ord.sheaf]
cover_le_trans [lemma, in semantics.ord.sheaf]
cover_le_refl [lemma, in semantics.ord.sheaf]
cover_le [definition, in semantics.ord.sheaf]
co_mono [instance, in semantics.tower.gfp_companion]
co_monotone [lemma, in semantics.tower.gfp_companion]
co_greatest_compatible [lemma, in semantics.tower.gfp_companion]
co_compatible [lemma, in semantics.tower.gfp_companion]
co_upto [lemma, in semantics.tower.gfp_companion]
CR [definition, in semantics.ars]
cr_method [lemma, in semantics.ars]
cr_conv_normal [lemma, in semantics.ars]
cr_star_normal [lemma, in semantics.ars]
ctm [abbreviation, in semantics.f.weaknorm]
ctx [definition, in semantics.ccomega.typing]
CtxOperator [constructor, in semantics.tower.ex_streams]
ctx_operator [inductive, in semantics.tower.ex_streams]
cvl [abbreviation, in semantics.f.weaknorm]
C_up [lemma, in semantics.f.strongnorm]
C_rename [lemma, in semantics.f.strongnorm]
C_scons [lemma, in semantics.f.strongnorm]
C_upto [lemma, in semantics.ccs.properties]
C_ctx [constructor, in semantics.ccs.properties]
C_trans [constructor, in semantics.ccs.properties]
C_sym [constructor, in semantics.ccs.properties]
C_bisim [constructor, in semantics.ccs.properties]
C_R [constructor, in semantics.ccs.properties]
C_inc [lemma, in semantics.tower.direct_induction]
C_lfp [lemma, in semantics.tower.direct_induction]
C_limit [constructor, in semantics.tower.direct_induction]
C_step [constructor, in semantics.tower.direct_induction]
D
D [definition, in semantics.f.weaknorm]D [definition, in semantics.f.strongnorm]
decreasing_is_below_companion [lemma, in semantics.tower.tower]
Def [constructor, in semantics.wp.ic]
Definitions [section, in semantics.ars]
Definitions.e [variable, in semantics.ars]
Definitions.T [variable, in semantics.ars]
deterministic [definition, in semantics.wp.abstract]
deterministic [definition, in semantics.wp.icsemantics]
deterministic_to_continuous [lemma, in semantics.wp.abstract]
deterministic_sup [lemma, in semantics.wp.abstract]
deterministic_sup_closed [lemma, in semantics.wp.icsemantics]
diamond [definition, in semantics.ars]
diamond_confluent [lemma, in semantics.ars]
directed [definition, in semantics.tower.direct_induction]
direct_induction [lemma, in semantics.tower.direct_induction]
direct_coinduction [lemma, in semantics.tower.direct_induction]
direct_induction [library]
distributes_over [definition, in semantics.wp.abstract]
distributive [definition, in semantics.wp.abstract]
Do [constructor, in semantics.wp.gc]
dual [definition, in semantics.ccs.semantics]
E
E [definition, in semantics.f.weaknorm]E [abbreviation, in semantics.f.strongnorm]
embed [definition, in semantics.ord.sheaf]
embedE [lemma, in semantics.ord.sheaf]
embedI [lemma, in semantics.ord.sheaf]
embedM [lemma, in semantics.ord.sheaf]
embedT [lemma, in semantics.ord.sheaf]
embed_unembed [lemma, in semantics.ord.sheaf]
embed_injective [lemma, in semantics.ord.sheaf]
embed_embedding [lemma, in semantics.ord.sheaf]
embed_cov [lemma, in semantics.ord.sheaf]
embed_def [lemma, in semantics.ord.sheaf]
equiv [record, in semantics.base.overture]
Equivalence [section, in semantics.base.overture]
EquivalencePaths [section, in semantics.base.fext]
EquivalencePaths.A [variable, in semantics.base.fext]
EquivalencePaths.B [variable, in semantics.base.fext]
Equivalence.A [variable, in semantics.base.overture]
Equivalence.B [variable, in semantics.base.overture]
equivmap [projection, in semantics.base.overture]
equivmap_is_equiv [projection, in semantics.base.overture]
EquivProp [section, in semantics.base.overture]
EquivProp.A [variable, in semantics.base.overture]
EquivProp.B [variable, in semantics.base.overture]
equiv_sect [lemma, in semantics.base.overture]
equiv_retr [lemma, in semantics.base.overture]
equiv_inverse [definition, in semantics.base.overture]
equiv_eq [lemma, in semantics.base.fext]
eq_star [lemma, in semantics.ars]
eval [definition, in semantics.f.types]
evaln [definition, in semantics.ars]
evalnP [lemma, in semantics.ars]
evaln_sound [lemma, in semantics.ars]
Evaluation [section, in semantics.f.types]
Evaluation.D [variable, in semantics.f.types]
Evaluation.M [variable, in semantics.f.types]
Evaluation.V [variable, in semantics.f.types]
eval_lift [lemma, in semantics.f.types]
eval_beta [lemma, in semantics.f.types]
eval_inst [lemma, in semantics.f.types]
eval_weaken [lemma, in semantics.f.types]
eval_ren [lemma, in semantics.f.types]
eweakening [lemma, in semantics.ccomega.contextmorphism]
exE [lemma, in semantics.ord.clat]
exEc [lemma, in semantics.ord.clat]
exI [lemma, in semantics.ord.clat]
exIc [lemma, in semantics.ord.clat]
exists_repr [lemma, in semantics.base.quotient]
exp [inductive, in semantics.ccs.syntax]
ext [inductive, in semantics.ccomega.typing]
ext_shift [constructor, in semantics.ccomega.typing]
ext_bound [constructor, in semantics.ccomega.typing]
ex_def [lemma, in semantics.ord.clat]
ex_mono [lemma, in semantics.ord.clat]
ex_axiom [lemma, in semantics.ord.clat]
ex_streams [library]
ex_similarity [library]
E_beta [lemma, in semantics.f.weaknorm]
E_tlam [lemma, in semantics.f.strongnorm]
E_tapp [lemma, in semantics.f.strongnorm]
E_lam [lemma, in semantics.f.strongnorm]
E_app [lemma, in semantics.f.strongnorm]
E_beta [lemma, in semantics.f.strongnorm]
E_weaken [lemma, in semantics.f.strongnorm]
E2_ind [lemma, in semantics.f.strongnorm]
F
Fbisim [definition, in semantics.ccs.bisim]Fbisim_mono [instance, in semantics.ccs.bisim]
fcbvreduction [library]
fcbvsyntax [library]
fext [definition, in semantics.base.fext]
fext [library]
fin [definition, in semantics.data.fintype]
fintype [library]
Fix [constructor, in semantics.ccs.syntax]
fix_proper [instance, in semantics.ccs.bisim]
flatmap [definition, in semantics.wp.compiler]
flip [definition, in semantics.ccs.bisim]
flip_symmetric [lemma, in semantics.ccs.bisim]
fp [record, in semantics.tower.tarski]
FpCLat [section, in semantics.tower.tarski]
FpCLat.f [variable, in semantics.tower.tarski]
FpCLat.X [variable, in semantics.tower.tarski]
fpP [projection, in semantics.tower.tarski]
fp_botE [lemma, in semantics.tower.tarski]
fp_topE [lemma, in semantics.tower.tarski]
fp_infP [lemma, in semantics.tower.tarski]
fp_inf [definition, in semantics.tower.tarski]
fp_leE [lemma, in semantics.tower.tarski]
fp_eq [lemma, in semantics.tower.tarski]
Frame [module, in semantics.ord.frame]
frame [library]
FrameLaws [section, in semantics.ord.frame]
FrameLaws.T [variable, in semantics.ord.frame]
Frame.base [projection, in semantics.ord.frame]
Frame.class [definition, in semantics.ord.frame]
Frame.Class [constructor, in semantics.ord.frame]
Frame.ClassDef [section, in semantics.ord.frame]
Frame.ClassDef.cT [variable, in semantics.ord.frame]
Frame.ClassDef.T [variable, in semantics.ord.frame]
Frame.ClassDef.xT [variable, in semantics.ord.frame]
Frame.class_of [record, in semantics.ord.frame]
Frame.clat [definition, in semantics.ord.frame]
Frame.clone [definition, in semantics.ord.frame]
Frame.Exports [module, in semantics.ord.frame]
Frame.Exports.Frame [abbreviation, in semantics.ord.frame]
Frame.Exports.frame [abbreviation, in semantics.ord.frame]
Frame.Exports.FrameMixin [abbreviation, in semantics.ord.frame]
[ frame of _ ] (form_scope) [notation, in semantics.ord.frame]
[ frame of _ for _ ] (form_scope) [notation, in semantics.ord.frame]
[ frameMixin of _ ] (form_scope) [notation, in semantics.ord.frame]
Frame.mixin [projection, in semantics.ord.frame]
Frame.Mixin [constructor, in semantics.ord.frame]
Frame.mixin_of [record, in semantics.ord.frame]
Frame.ordType [definition, in semantics.ord.frame]
Frame.pack [definition, in semantics.ord.frame]
Frame.Pack [constructor, in semantics.ord.frame]
Frame.proType [definition, in semantics.ord.frame]
Frame.sort [projection, in semantics.ord.frame]
Frame.type [record, in semantics.ord.frame]
Frame.xclass [abbreviation, in semantics.ord.frame]
fsemantics [library]
Fsim [definition, in semantics.ccs.bisim]
Fsim_mono [instance, in semantics.ccs.bisim]
fsyntax [library]
fundamental [lemma, in semantics.f.weaknorm]
fundamental [lemma, in semantics.f.strongnorm]
f_omega_cocont_strong [lemma, in semantics.tower.cocontinuous_tower]
G
gc [definition, in semantics.wp.gc]gc [library]
GCInduction [section, in semantics.wp.gc]
GCInduction.P [variable, in semantics.wp.gc]
GCInduction.p_do [variable, in semantics.wp.gc]
GCInduction.p_case [variable, in semantics.wp.gc]
GCInduction.p_seq [variable, in semantics.wp.gc]
GCInduction.p_assn [variable, in semantics.wp.gc]
GCInduction.p_skip [variable, in semantics.wp.gc]
GCInduction.Q [variable, in semantics.wp.gc]
GCInduction.q_cons [variable, in semantics.wp.gc]
GCInduction.q_nil [variable, in semantics.wp.gc]
gcsemantics [library]
gc_ind [definition, in semantics.wp.gc]
gc_ind' [definition, in semantics.wp.gc]
gfp [definition, in semantics.tower.tarski]
GfpCompanion [section, in semantics.tower.gfp_companion]
GfpCompanion.f [variable, in semantics.tower.gfp_companion]
GfpCompanion.f_mono [variable, in semantics.tower.gfp_companion]
GfpCompanion.X [variable, in semantics.tower.gfp_companion]
gfpE [lemma, in semantics.tower.tarski]
gfp_const [lemma, in semantics.wp.compiler]
gfp_mono [instance, in semantics.wp.compiler]
gfp_def [lemma, in semantics.tower.tarski]
gfp_belowE [lemma, in semantics.tower.tarski]
gfp_below_unfold [lemma, in semantics.tower.tarski]
gfp_below_le [lemma, in semantics.tower.tarski]
gfp_below_coind [lemma, in semantics.tower.tarski]
gfp_below [definition, in semantics.tower.tarski]
gfp_companion [library]
glbE [lemma, in semantics.ord.protype]
GlbOrder [section, in semantics.ord.ordtype]
GlbOrder.f [variable, in semantics.ord.ordtype]
GlbOrder.T [variable, in semantics.ord.ordtype]
GlbOrder.X [variable, in semantics.ord.ordtype]
GlbOrder.Y [variable, in semantics.ord.ordtype]
glbP [lemma, in semantics.ord.protype]
GlbPreorder [section, in semantics.ord.protype]
GlbPreorder.f [variable, in semantics.ord.protype]
GlbPreorder.T [variable, in semantics.ord.protype]
GlbPreorder.X [variable, in semantics.ord.protype]
GlbPreorder.Y [variable, in semantics.ord.protype]
glb_uniq [lemma, in semantics.ord.ordtype]
glb_lb [lemma, in semantics.ord.protype]
Gtest [definition, in semantics.wp.gcsemantics]
gtest [definition, in semantics.wp.gcsemantics]
gtestP [lemma, in semantics.wp.compiler]
gtest_contra [lemma, in semantics.wp.compiler]
gtest_cons [lemma, in semantics.wp.compiler]
guard [definition, in semantics.ccs.semantics]
guard [axiom, in semantics.wp.states]
guardE [axiom, in semantics.wp.states]
guard_eqP [axiom, in semantics.wp.states]
guard_eq [axiom, in semantics.wp.states]
H
has_type_ind [definition, in semantics.f.weaknorm]has_type [inductive, in semantics.f.fsemantics]
has_type [inductive, in semantics.ccomega.typing]
hex [definition, in semantics.base.inhab]
hex_rec_prop [definition, in semantics.base.inhab]
hex_ind [definition, in semantics.base.inhab]
hex_rec [definition, in semantics.base.inhab]
hex_rect [definition, in semantics.base.inhab]
HoareRules [section, in semantics.wp.gcsemantics]
hoare_do [lemma, in semantics.wp.gcsemantics]
hoare_case [lemma, in semantics.wp.gcsemantics]
hoare_seq [lemma, in semantics.wp.gcsemantics]
hoare_act [lemma, in semantics.wp.gcsemantics]
hoare_skip [lemma, in semantics.wp.gcsemantics]
hprop [record, in semantics.base.overture]
hpropP [definition, in semantics.base.overture]
hprop_is_prop [projection, in semantics.base.overture]
hprop_type [projection, in semantics.base.overture]
I
ic [library]icsemantics [library]
ids [definition, in semantics.ccs.syntax]
id_rcomp [lemma, in semantics.ccs.syntax]
id_inst [lemma, in semantics.ccs.syntax]
If [constructor, in semantics.wp.ic]
imp [definition, in semantics.ord.frame]
impBx [lemma, in semantics.ord.frame]
impEl [lemma, in semantics.ord.frame]
impEr [lemma, in semantics.ord.frame]
impEx [lemma, in semantics.ord.frame]
impI [lemma, in semantics.ord.frame]
impJx [lemma, in semantics.ord.frame]
impl_prop_subrelation [instance, in semantics.ord.prop]
impMx [lemma, in semantics.ord.frame]
impP [lemma, in semantics.ord.frame]
impTx [lemma, in semantics.ord.frame]
impxA [lemma, in semantics.ord.frame]
impxJ [lemma, in semantics.ord.frame]
impxM [lemma, in semantics.ord.frame]
impxT [lemma, in semantics.ord.frame]
impxx [lemma, in semantics.ord.frame]
imp_def [lemma, in semantics.ord.frame]
imp_cut [lemma, in semantics.ord.frame]
imp_proper [instance, in semantics.ord.frame]
InducedOrder [section, in semantics.ord.ordtype]
InducedOrder.f [variable, in semantics.ord.ordtype]
InducedOrder.f_inj [variable, in semantics.ord.ordtype]
InducedOrder.T [variable, in semantics.ord.ordtype]
InducedOrder.X [variable, in semantics.ord.ordtype]
InducedOrdType [abbreviation, in semantics.ord.ordtype]
InducedPreorder [section, in semantics.ord.protype]
InducedPreorder.f [variable, in semantics.ord.protype]
InducedPreorder.T [variable, in semantics.ord.protype]
InducedPreorder.X [variable, in semantics.ord.protype]
InducedProType [abbreviation, in semantics.ord.protype]
induced_le_eq [lemma, in semantics.ord.ordtype]
induced_le_trans [lemma, in semantics.ord.protype]
induced_le_refl [lemma, in semantics.ord.protype]
induced_le [definition, in semantics.ord.protype]
inf [definition, in semantics.ord.clat]
InfClosedCoinduction [section, in semantics.tower.direct_induction]
InfClosedCoinduction.f [variable, in semantics.tower.direct_induction]
InfClosedCoinduction.fP [variable, in semantics.tower.direct_induction]
InfClosedCoinduction.H [variable, in semantics.tower.direct_induction]
InfClosedCoinduction.P [variable, in semantics.tower.direct_induction]
InfClosedCoinduction.X [variable, in semantics.tower.direct_induction]
infguard [definition, in semantics.ord.clat]
inf_closed_to_closure_retr [lemma, in semantics.tower.associated_closure]
inf_closed_to_closure [definition, in semantics.tower.associated_closure]
inf_closed_wpi_distributive [lemma, in semantics.wp.icsemantics]
inf_closed [definition, in semantics.ord.clat]
inf_closed_coind [lemma, in semantics.tower.direct_induction]
inf_closed_wp_distributive [lemma, in semantics.wp.gcsemantics]
Inhab [module, in semantics.base.inhab]
inhab [library]
inhab_prop [lemma, in semantics.base.inhab]
inhab_indP [definition, in semantics.base.inhab]
inhab_ind [definition, in semantics.base.inhab]
inhab_rec [definition, in semantics.base.inhab]
inhab_map_is_equiv [definition, in semantics.base.fext]
inhab_map_retr [lemma, in semantics.base.fext]
inhab_map_sect [lemma, in semantics.base.fext]
inhab_map [definition, in semantics.base.fext]
Inhab.Induction [section, in semantics.base.inhab]
Inhab.inhab [inductive, in semantics.base.inhab]
Inhab.inhab_rect [definition, in semantics.base.inhab]
Inhab.tr [constructor, in semantics.base.inhab]
Inhab.trP [axiom, in semantics.base.inhab]
InjectiveSurjective [section, in semantics.base.inhab]
InjectiveSurjective.A [variable, in semantics.base.inhab]
InjectiveSurjective.B [variable, in semantics.base.inhab]
InjectiveSurjective.f [variable, in semantics.base.inhab]
InjectiveSurjective.f_surj [variable, in semantics.base.inhab]
InjectiveSurjective.f_inj [variable, in semantics.base.inhab]
injP [lemma, in semantics.wp.gc]
inj_prod [lemma, in semantics.ccomega.churchrosser]
inj_sort [lemma, in semantics.ccomega.churchrosser]
inst [definition, in semantics.wp.ic]
inst [definition, in semantics.f.fsyntax]
inst [definition, in semantics.debruijn.syntax]
inst [definition, in semantics.ccomega.syntax]
inst_comp [lemma, in semantics.wp.ic]
inst_rinst_comp [lemma, in semantics.wp.ic]
inst_ids [lemma, in semantics.wp.ic]
inst_id [lemma, in semantics.ccs.syntax]
inst_comp [lemma, in semantics.f.fsyntax]
inst_ren_comp [lemma, in semantics.f.fsyntax]
inst_ids [lemma, in semantics.f.fsyntax]
inst_comp [lemma, in semantics.debruijn.syntax]
inst_ren_comp [lemma, in semantics.debruijn.syntax]
inst_ids [lemma, in semantics.debruijn.syntax]
inst_shift [lemma, in semantics.debruijn.syntax]
inst_bound [lemma, in semantics.debruijn.syntax]
inst_lam [lemma, in semantics.debruijn.syntax]
inst_app [lemma, in semantics.debruijn.syntax]
inst_comp [lemma, in semantics.ccomega.syntax]
inst_ren_comp [lemma, in semantics.ccomega.syntax]
inst_ids [lemma, in semantics.ccomega.syntax]
interior [definition, in semantics.tower.reals]
interval [record, in semantics.tower.reals]
interval [definition, in semantics.base.fext]
Interval [section, in semantics.base.fext]
IntervalDomain [section, in semantics.tower.reals]
_ ^- [notation, in semantics.tower.reals]
_ ^+ [notation, in semantics.tower.reals]
interval_lt_inf [lemma, in semantics.tower.reals]
interval_lt_right [lemma, in semantics.tower.reals]
interval_lt_left [lemma, in semantics.tower.reals]
interval_lt [definition, in semantics.tower.reals]
interval_inf_axiom [lemma, in semantics.tower.reals]
interval_inf [definition, in semantics.tower.reals]
interval_le_eq [lemma, in semantics.tower.reals]
interval_le_trans [lemma, in semantics.tower.reals]
interval_le_refl [lemma, in semantics.tower.reals]
interval_le [definition, in semantics.tower.reals]
interval_eq [lemma, in semantics.tower.reals]
interval_lower_lt_upper [projection, in semantics.tower.reals]
Interval.i0 [variable, in semantics.base.fext]
Interval.i1 [variable, in semantics.base.fext]
inverse [projection, in semantics.base.overture]
inverse_cr [projection, in semantics.base.overture]
inverse_cl [projection, in semantics.base.overture]
inverse_cand_retraction [lemma, in semantics.base.inhab]
inverse_cand_section [lemma, in semantics.base.inhab]
inverse_cand [definition, in semantics.base.inhab]
in_classE [lemma, in semantics.base.quotient]
in_class [definition, in semantics.base.quotient]
iprod [definition, in semantics.base.overture]
IProdCLat [section, in semantics.ord.prod]
IProdCLat.F [variable, in semantics.ord.prod]
IProdCLat.T [variable, in semantics.ord.prod]
IProdFrame [section, in semantics.ord.prod]
IProdFrame.F [variable, in semantics.ord.prod]
IProdFrame.T [variable, in semantics.ord.prod]
IProdLLat [section, in semantics.tower.llat]
IProdLLat.F [variable, in semantics.tower.llat]
IProdLLat.T [variable, in semantics.tower.llat]
IProdOrdType [section, in semantics.ord.prod]
IProdOrdType.F [variable, in semantics.ord.prod]
IProdOrdType.T [variable, in semantics.ord.prod]
IProdProType [section, in semantics.ord.prod]
IProdProType.F [variable, in semantics.ord.prod]
IProdProType.T [variable, in semantics.ord.prod]
iprod_leE [lemma, in semantics.ord.prod]
iprod_impE [lemma, in semantics.ord.prod]
iprod_frameP [lemma, in semantics.ord.prod]
iprod_allE [lemma, in semantics.ord.prod]
iprod_exE [lemma, in semantics.ord.prod]
iprod_meetE [lemma, in semantics.ord.prod]
iprod_joinE [lemma, in semantics.ord.prod]
iprod_botE [lemma, in semantics.ord.prod]
iprod_topE [lemma, in semantics.ord.prod]
iprod_infP [lemma, in semantics.ord.prod]
iprod_inf [definition, in semantics.ord.prod]
iprod_le_eq [lemma, in semantics.ord.prod]
iprod_le_trans [lemma, in semantics.ord.prod]
iprod_le_refl [lemma, in semantics.ord.prod]
iprod_le [definition, in semantics.ord.prod]
iprod_lt_inf [lemma, in semantics.tower.llat]
iprod_lt_right [lemma, in semantics.tower.llat]
iprod_lt_left [lemma, in semantics.tower.llat]
iprod_lt [definition, in semantics.tower.llat]
is_glb [definition, in semantics.ord.protype]
is_lb [definition, in semantics.ord.protype]
is_lub [definition, in semantics.ord.protype]
is_ub [definition, in semantics.ord.protype]
is_equiv_comp [definition, in semantics.base.overture]
is_equiv_inv [definition, in semantics.base.overture]
is_equiv_idfun [definition, in semantics.base.overture]
is_equiv [record, in semantics.base.overture]
is_prop [definition, in semantics.base.overture]
is_type [definition, in semantics.ccomega.typing]
is_cocontinuous [definition, in semantics.tower.cocontinuous_tower]
is_continuous [record, in semantics.ord.cont]
is_type_weakening [lemma, in semantics.ccomega.subjectreduction]
is_finite_lam [lemma, in semantics.ccomega.subjectreduction]
is_finite_prod [lemma, in semantics.ccomega.subjectreduction]
is_finite_var [lemma, in semantics.ccomega.subjectreduction]
is_finite_ext [constructor, in semantics.ccomega.subjectreduction]
is_finite_empty [constructor, in semantics.ccomega.subjectreduction]
is_finite [inductive, in semantics.ccomega.subjectreduction]
is_equiv_prop [lemma, in semantics.base.fext]
is_kernel_counit [instance, in semantics.ord.adj]
is_closure_kernel_rev [instance, in semantics.ord.adj]
is_kernel_closure_rev [instance, in semantics.ord.adj]
is_kernel [definition, in semantics.ord.adj]
is_closure_unit [instance, in semantics.ord.adj]
is_closure [definition, in semantics.ord.adj]
is_adjunction [definition, in semantics.ord.adj]
is_subcanonical [definition, in semantics.ord.sheaf]
is_sheaf_exponential_ideal [lemma, in semantics.ord.sheaf]
is_sheaf_inf_closed [lemma, in semantics.ord.sheaf]
is_sheaf [definition, in semantics.ord.sheaf]
iter_mono [lemma, in semantics.wp.prelim]
I_path [lemma, in semantics.base.fext]
J
J [definition, in semantics.base.overture]JLatLaws [section, in semantics.ord.clat]
JLatLaws.T [variable, in semantics.ord.clat]
join [definition, in semantics.ord.clat]
joinA [lemma, in semantics.ord.clat]
joinable [definition, in semantics.ars]
joinAC [lemma, in semantics.ord.clat]
joinACA [lemma, in semantics.ord.clat]
joinBx [lemma, in semantics.ord.clat]
joinC [lemma, in semantics.ord.clat]
joinCA [lemma, in semantics.ord.clat]
joinE [lemma, in semantics.ord.clat]
joinIl [lemma, in semantics.ord.clat]
joinIr [lemma, in semantics.ord.clat]
joinKx [lemma, in semantics.ord.clat]
joinTx [lemma, in semantics.ord.clat]
joinxB [lemma, in semantics.ord.clat]
joinxK [lemma, in semantics.ord.clat]
joinxT [lemma, in semantics.ord.clat]
joinxx [lemma, in semantics.ord.clat]
join_conv [lemma, in semantics.ars]
join_def [lemma, in semantics.ord.clat]
join_proper [instance, in semantics.ord.clat]
join_mono [lemma, in semantics.ord.clat]
join_axiom [lemma, in semantics.ord.clat]
Jump [constructor, in semantics.wp.ic]
K
K [abbreviation, in semantics.f.strongnorm]K [definition, in semantics.base.pext]
KernelOperationsOrder [section, in semantics.ord.adj]
KernelOperationsOrder.Xr [variable, in semantics.ord.adj]
KernelOperators [section, in semantics.ord.adj]
KernelOperators.Xr [variable, in semantics.ord.adj]
kernelP [lemma, in semantics.ord.adj]
kernel_lub [lemma, in semantics.ord.adj]
kernel_glb [lemma, in semantics.ord.adj]
kernel_stable [lemma, in semantics.ord.adj]
kernel_eq [lemma, in semantics.ord.adj]
kernel_idem [lemma, in semantics.ord.adj]
kernel_dec [lemma, in semantics.ord.adj]
Kleene [section, in semantics.wp.prelim]
kleene_fp [lemma, in semantics.wp.prelim]
kleene_t_is_t [lemma, in semantics.tower.cocontinuous_tower]
kleene_compat [lemma, in semantics.tower.cocontinuous_tower]
kleene_t_mono [instance, in semantics.tower.cocontinuous_tower]
kleene_t [definition, in semantics.tower.cocontinuous_tower]
Kleene.f [variable, in semantics.wp.prelim]
Kleene.f_cont [variable, in semantics.wp.prelim]
Kleene.f_mono [variable, in semantics.wp.prelim]
Kleene.X [variable, in semantics.wp.prelim]
K_weaken [lemma, in semantics.f.strongnorm]
K_all [lemma, in semantics.f.strongnorm]
K_arr [lemma, in semantics.f.strongnorm]
K_var [lemma, in semantics.f.strongnorm]
L
L [definition, in semantics.f.weaknorm]lam [constructor, in semantics.f.fsyntax]
lam [constructor, in semantics.debruijn.syntax]
lam [constructor, in semantics.ccomega.syntax]
lam [constructor, in semantics.f.fcbvsyntax]
LatLaws [section, in semantics.ord.clat]
LatLaws.T [variable, in semantics.ord.clat]
lbP [lemma, in semantics.ord.protype]
LeftAdjoints [section, in semantics.ord.adj]
LetDef [definition, in semantics.wp.compiler]
le_eq [lemma, in semantics.ord.ordtype]
le_trans [lemma, in semantics.ord.protype]
le_refl [lemma, in semantics.ord.protype]
le_meetP [lemma, in semantics.ord.clat]
le_joinP [lemma, in semantics.ord.clat]
lfp [definition, in semantics.tower.tarski]
lfpE [lemma, in semantics.tower.tarski]
lfp_const [lemma, in semantics.wp.compiler]
lfp_mono [instance, in semantics.wp.compiler]
lfp_approx [definition, in semantics.wp.icsemantics]
lfp_def [lemma, in semantics.tower.tarski]
lfp_aboveE [lemma, in semantics.tower.tarski]
lfp_above_fold [lemma, in semantics.tower.tarski]
lfp_above_ge [lemma, in semantics.tower.tarski]
lfp_above_ind [lemma, in semantics.tower.tarski]
lfp_above [definition, in semantics.tower.tarski]
lift [definition, in semantics.f.types]
LinearTower [section, in semantics.tower.linear_tower]
LinearTower.f [variable, in semantics.tower.linear_tower]
LinearTower.f_mono [variable, in semantics.tower.linear_tower]
LinearTower.X [variable, in semantics.tower.linear_tower]
linear_tower [library]
LLat [module, in semantics.tower.llat]
llat [library]
LLatLemmas [section, in semantics.tower.llat]
LLatLemmas.T [variable, in semantics.tower.llat]
LLat.base [projection, in semantics.tower.llat]
LLat.class [definition, in semantics.tower.llat]
LLat.Class [constructor, in semantics.tower.llat]
LLat.ClassDef [section, in semantics.tower.llat]
LLat.ClassDef.cT [variable, in semantics.tower.llat]
LLat.ClassDef.T [variable, in semantics.tower.llat]
LLat.ClassDef.xT [variable, in semantics.tower.llat]
LLat.class_of [record, in semantics.tower.llat]
LLat.clat [definition, in semantics.tower.llat]
LLat.clone [definition, in semantics.tower.llat]
LLat.Exports [module, in semantics.tower.llat]
LLat.Exports.LLat [abbreviation, in semantics.tower.llat]
LLat.Exports.llat [abbreviation, in semantics.tower.llat]
LLat.Exports.LLatMixin [abbreviation, in semantics.tower.llat]
[ llat of _ ] (form_scope) [notation, in semantics.tower.llat]
[ llat of _ for _ ] (form_scope) [notation, in semantics.tower.llat]
[ llatMixin of _ ] (form_scope) [notation, in semantics.tower.llat]
LLat.lt [projection, in semantics.tower.llat]
LLat.mixin [projection, in semantics.tower.llat]
LLat.Mixin [constructor, in semantics.tower.llat]
LLat.mixin_of [record, in semantics.tower.llat]
LLat.ordType [definition, in semantics.tower.llat]
LLat.pack [definition, in semantics.tower.llat]
LLat.Pack [constructor, in semantics.tower.llat]
LLat.proType [definition, in semantics.tower.llat]
LLat.sort [projection, in semantics.tower.llat]
LLat.type [record, in semantics.tower.llat]
LLat.xclass [abbreviation, in semantics.tower.llat]
lmonoP [projection, in semantics.tower.llat]
lmonotone [record, in semantics.tower.llat]
lmonotone_to_monotone [projection, in semantics.tower.llat]
loop [definition, in semantics.tower.ex_similarity]
loop_countable_branching_not_similar [lemma, in semantics.tower.ex_similarity]
loop_countable_branching_nsim [lemma, in semantics.tower.ex_similarity]
lower_uopen [projection, in semantics.tower.reals]
lower_lset [projection, in semantics.tower.reals]
lower_interval [projection, in semantics.tower.reals]
lprop [record, in semantics.tower.llat]
lts [definition, in semantics.ccs.semantics]
lts [record, in semantics.tower.ex_similarity]
lts_nodes [projection, in semantics.tower.ex_similarity]
lt_inf [lemma, in semantics.tower.llat]
lt_right [lemma, in semantics.tower.llat]
lt_left [lemma, in semantics.tower.llat]
lubE [lemma, in semantics.ord.protype]
LubOrder [section, in semantics.ord.ordtype]
LubOrder.f [variable, in semantics.ord.ordtype]
LubOrder.T [variable, in semantics.ord.ordtype]
LubOrder.X [variable, in semantics.ord.ordtype]
lubP [lemma, in semantics.ord.protype]
LubPreorder [section, in semantics.ord.protype]
LubPreorder.f [variable, in semantics.ord.protype]
LubPreorder.T [variable, in semantics.ord.protype]
LubPreorder.X [variable, in semantics.ord.protype]
lub_uniq [lemma, in semantics.ord.ordtype]
lub_ub [lemma, in semantics.ord.protype]
M
M [definition, in semantics.f.strongnorm]map_subst [lemma, in semantics.ccs.syntax]
map_quot [definition, in semantics.base.quotient]
map_inhab [definition, in semantics.base.fext]
mceil [definition, in semantics.ord.mfun]
mceil_is_adjunction [instance, in semantics.ord.mfun]
meet [definition, in semantics.ord.clat]
meetA [lemma, in semantics.ord.clat]
meetAC [lemma, in semantics.ord.clat]
meetACA [lemma, in semantics.ord.clat]
meetBx [lemma, in semantics.ord.clat]
meetC [lemma, in semantics.ord.clat]
meetCA [lemma, in semantics.ord.clat]
meetEl [lemma, in semantics.ord.clat]
meetEr [lemma, in semantics.ord.clat]
meetEx [lemma, in semantics.ord.frame]
meetHl [lemma, in semantics.ord.frame]
meetHr [lemma, in semantics.ord.frame]
meetI [lemma, in semantics.ord.clat]
meetJx [lemma, in semantics.ord.frame]
meetKx [lemma, in semantics.ord.clat]
meetTx [lemma, in semantics.ord.clat]
meetxB [lemma, in semantics.ord.clat]
meetxE [lemma, in semantics.ord.frame]
meetxJ [lemma, in semantics.ord.frame]
meetxK [lemma, in semantics.ord.clat]
meetxT [lemma, in semantics.ord.clat]
meetxx [lemma, in semantics.ord.clat]
meet_def [lemma, in semantics.ord.clat]
meet_proper [instance, in semantics.ord.clat]
meet_mono [lemma, in semantics.ord.clat]
meet_axiom [lemma, in semantics.ord.clat]
meta [library]
mfloor [definition, in semantics.ord.mfun]
mfloor_is_adjunction [instance, in semantics.ord.mfun]
MFun [section, in semantics.ord.mfun]
mfun [constructor, in semantics.ord.mfun]
mfun [library]
MFunCLat [section, in semantics.ord.mfun]
MFunCLat.X [variable, in semantics.ord.mfun]
MFunCLat.Y [variable, in semantics.ord.mfun]
MFunFrame [section, in semantics.ord.mfun]
MFunFrame.X [variable, in semantics.ord.mfun]
MFunFrame.Y [variable, in semantics.ord.mfun]
mfun_impE [lemma, in semantics.ord.mfun]
mfun_frameP [lemma, in semantics.ord.mfun]
mfun_allE [lemma, in semantics.ord.mfun]
mfun_exE [lemma, in semantics.ord.mfun]
mfun_meetE [lemma, in semantics.ord.mfun]
mfun_joinE [lemma, in semantics.ord.mfun]
mfun_botE [lemma, in semantics.ord.mfun]
mfun_topE [lemma, in semantics.ord.mfun]
mfun_infP [lemma, in semantics.ord.mfun]
mfun_inf [definition, in semantics.ord.mfun]
mfun_leE [lemma, in semantics.ord.mfun]
mfun_eq [lemma, in semantics.ord.mfun]
mfun_proper [instance, in semantics.ord.mfun]
mfun_monotone [instance, in semantics.ord.mfun]
mfun_of [definition, in semantics.ord.mfun]
mfun_type [record, in semantics.ord.mfun]
MFun.X [variable, in semantics.ord.mfun]
MFun.Y [variable, in semantics.ord.mfun]
mk_glb [lemma, in semantics.ord.protype]
mk_lub [lemma, in semantics.ord.protype]
mk_mfun [definition, in semantics.ord.mfun]
mk_interval [constructor, in semantics.tower.reals]
mk_equiv [constructor, in semantics.base.overture]
mk_is_equiv [constructor, in semantics.base.overture]
mk_hprop [constructor, in semantics.base.overture]
mk_model [constructor, in semantics.f.types]
mk_lprop [constructor, in semantics.tower.llat]
mk_is_continuous [constructor, in semantics.ord.cont]
mk_fp [constructor, in semantics.tower.tarski]
mk_lts [constructor, in semantics.tower.ex_similarity]
mk_sieve [constructor, in semantics.ord.sheaf]
mk_sheaf [constructor, in semantics.ord.sheaf]
mk_basis_pred [constructor, in semantics.ord.sheaf]
MLatLaws [section, in semantics.ord.clat]
MLatLaws.T [variable, in semantics.ord.clat]
model [record, in semantics.f.types]
mono [lemma, in semantics.ord.mono]
mono [library]
monoA [lemma, in semantics.ord.mono]
monoAc [lemma, in semantics.ord.mono]
MonoCLat [section, in semantics.ord.mono]
MonoCLat.f [variable, in semantics.ord.mono]
MonoCLat.X [variable, in semantics.ord.mono]
MonoCLat.Y [variable, in semantics.ord.mono]
monoE [lemma, in semantics.ord.mono]
monoEc [lemma, in semantics.ord.mono]
monofun [projection, in semantics.ord.mfun]
monofun_is_proper [instance, in semantics.ord.mfun]
monoJ [lemma, in semantics.ord.mono]
monoM [lemma, in semantics.ord.mono]
monotone [definition, in semantics.ord.mono]
monotone_yo [instance, in semantics.ord.presheaf]
monotone_monofun [projection, in semantics.ord.mfun]
monotone_proper [instance, in semantics.ord.mono]
monotone_kernel [instance, in semantics.ord.adj]
monotone_closure [instance, in semantics.ord.adj]
monotone_unembed [lemma, in semantics.ord.sheaf]
monotone_embed [instance, in semantics.ord.sheaf]
mstep [abbreviation, in semantics.wp.icsemantics]
N
nat_le_E [lemma, in semantics.ccomega.sorts]nat_le_eq [lemma, in semantics.ccomega.sorts]
nat_le_trans [lemma, in semantics.ccomega.sorts]
nat_le_refl [lemma, in semantics.ccomega.sorts]
nat_le [definition, in semantics.ccomega.sorts]
neq [definition, in semantics.tower.ex_streams]
New [constructor, in semantics.ccs.syntax]
new_proper [instance, in semantics.ccs.bisim]
nf [definition, in semantics.ars]
nf_accn [lemma, in semantics.ars]
NGtest [definition, in semantics.wp.gcsemantics]
normal [definition, in semantics.ars]
normalizing [definition, in semantics.ars]
normal_star [lemma, in semantics.ars]
normal_step_sort [lemma, in semantics.ccomega.churchrosser]
nsim [definition, in semantics.tower.ex_similarity]
null [definition, in semantics.data.fintype]
O
obisim [abbreviation, in semantics.ccs.bisim]OBisim [definition, in semantics.ccs.bisim]
obisim_unfold_mu [lemma, in semantics.ccs.bisim]
obisim_equiv [instance, in semantics.ccs.bisim]
obisim_coind [lemma, in semantics.ccs.bisim]
observable [definition, in semantics.ccs.semantics]
Ord [module, in semantics.ord.ordtype]
ord [library]
ordtype [library]
ord_op_preord [instance, in semantics.ord.protype]
ord_op_trans [instance, in semantics.ord.protype]
ord_op_refl [instance, in semantics.ord.protype]
ord_op_rew [instance, in semantics.ord.protype]
ord_op [definition, in semantics.ord.protype]
ord_l_op [definition, in semantics.tower.llat]
Ord.base [projection, in semantics.ord.ordtype]
Ord.class [definition, in semantics.ord.ordtype]
Ord.Class [constructor, in semantics.ord.ordtype]
Ord.ClassDef [section, in semantics.ord.ordtype]
Ord.ClassDef.cT [variable, in semantics.ord.ordtype]
Ord.ClassDef.T [variable, in semantics.ord.ordtype]
Ord.ClassDef.xT [variable, in semantics.ord.ordtype]
Ord.class_of [record, in semantics.ord.ordtype]
Ord.clone [definition, in semantics.ord.ordtype]
Ord.Exports [module, in semantics.ord.ordtype]
Ord.Exports.OrdMixin [abbreviation, in semantics.ord.ordtype]
Ord.Exports.OrdType [abbreviation, in semantics.ord.ordtype]
Ord.Exports.ordType [abbreviation, in semantics.ord.ordtype]
[ ordType of _ ] (form_scope) [notation, in semantics.ord.ordtype]
[ ordType of _ for _ ] (form_scope) [notation, in semantics.ord.ordtype]
[ ordMixin of _ ] (form_scope) [notation, in semantics.ord.ordtype]
Ord.mixin [projection, in semantics.ord.ordtype]
Ord.Mixin [constructor, in semantics.ord.ordtype]
Ord.mixin_of [record, in semantics.ord.ordtype]
Ord.pack [definition, in semantics.ord.ordtype]
Ord.Pack [constructor, in semantics.ord.ordtype]
Ord.proType [definition, in semantics.ord.ordtype]
Ord.sort [projection, in semantics.ord.ordtype]
Ord.type [record, in semantics.ord.ordtype]
Ord.xclass [abbreviation, in semantics.ord.ordtype]
overture [library]
P
pack_induced_ordType [definition, in semantics.ord.ordtype]pack_induced_proType [definition, in semantics.ord.protype]
pairb [definition, in semantics.base.fext]
pairb_fun [lemma, in semantics.base.fext]
PairCLat [section, in semantics.ord.prod]
PairCLat.A [variable, in semantics.ord.prod]
PairCLat.B [variable, in semantics.ord.prod]
PairFrame [section, in semantics.ord.prod]
PairFrame.A [variable, in semantics.ord.prod]
PairFrame.B [variable, in semantics.ord.prod]
PairOrdType [section, in semantics.ord.prod]
PairOrdType.A [variable, in semantics.ord.prod]
PairOrdType.B [variable, in semantics.ord.prod]
PairProType [section, in semantics.ord.prod]
PairProType.A [variable, in semantics.ord.prod]
PairProType.B [variable, in semantics.ord.prod]
pair_impE [lemma, in semantics.ord.prod]
pair_frameP [lemma, in semantics.ord.prod]
pair_allE [lemma, in semantics.ord.prod]
pair_exE [lemma, in semantics.ord.prod]
pair_meetE [lemma, in semantics.ord.prod]
pair_joinE [lemma, in semantics.ord.prod]
pair_botE [lemma, in semantics.ord.prod]
pair_topE [lemma, in semantics.ord.prod]
pair_infP [lemma, in semantics.ord.prod]
pair_inf [definition, in semantics.ord.prod]
pair_le_eq [lemma, in semantics.ord.prod]
pair_le_trans [lemma, in semantics.ord.prod]
pair_le_refl [lemma, in semantics.ord.prod]
pair_le [definition, in semantics.ord.prod]
Par [constructor, in semantics.ccs.syntax]
parameterized [library]
ParameterizedTower [section, in semantics.tower.parameterized]
ParameterizedTower.A [variable, in semantics.tower.parameterized]
ParameterizedTower.f [variable, in semantics.tower.parameterized]
ParameterizedTower.f_mono [variable, in semantics.tower.parameterized]
parameterized_tower_ind_s [lemma, in semantics.tower.parameterized]
parameterized_tower_ind [lemma, in semantics.tower.parameterized]
par_proper [instance, in semantics.ccs.bisim]
Pataraia [module, in semantics.tower.direct_induction]
Pataraia.infl [record, in semantics.tower.direct_induction]
Pataraia.infl_nullP [lemma, in semantics.tower.direct_induction]
Pataraia.infl_null_T [lemma, in semantics.tower.direct_induction]
Pataraia.infl_codirected [lemma, in semantics.tower.direct_induction]
Pataraia.infl_null [definition, in semantics.tower.direct_induction]
Pataraia.infl_comp [lemma, in semantics.tower.direct_induction]
Pataraia.infl_id [lemma, in semantics.tower.direct_induction]
Pataraia.infl_f [lemma, in semantics.tower.direct_induction]
Pataraia.infl_T [projection, in semantics.tower.direct_induction]
Pataraia.infl_dec [projection, in semantics.tower.direct_induction]
Pataraia.infl_mono [projection, in semantics.tower.direct_induction]
Pataraia.T [inductive, in semantics.tower.direct_induction]
Pataraia.T_dec [lemma, in semantics.tower.direct_induction]
Pataraia.T_top [lemma, in semantics.tower.direct_induction]
Pataraia.T_limit [constructor, in semantics.tower.direct_induction]
Pataraia.T_step [constructor, in semantics.tower.direct_induction]
Pataraia.WithFunction [section, in semantics.tower.direct_induction]
Pataraia.WithFunction.A [variable, in semantics.tower.direct_induction]
Pataraia.WithFunction.f [variable, in semantics.tower.direct_induction]
Pataraia.WithFunction.f_mono [variable, in semantics.tower.direct_induction]
Pataraia.ν [definition, in semantics.tower.direct_induction]
Pataraia.ν_gfp [lemma, in semantics.tower.direct_induction]
Pataraia.ν_coind [lemma, in semantics.tower.direct_induction]
Pataraia.ν_min [lemma, in semantics.tower.direct_induction]
Pataraia.ν_inc [lemma, in semantics.tower.direct_induction]
Pataraia.ν_tower [lemma, in semantics.tower.direct_induction]
path_I [definition, in semantics.base.fext]
pext [lemma, in semantics.base.pext]
pext [library]
pi [lemma, in semantics.base.pext]
point [projection, in semantics.tower.tarski]
Pred [definition, in semantics.base.overture]
prelim [library]
PreorderLemmas [section, in semantics.ord.protype]
PreorderLemmas.T [variable, in semantics.ord.protype]
presheaf [abbreviation, in semantics.ord.presheaf]
presheaf [library]
PresheafLaws [section, in semantics.ord.presheaf]
PresheafLaws.X [variable, in semantics.ord.presheaf]
presheafP [lemma, in semantics.ord.presheaf]
PresheafType [section, in semantics.ord.presheaf]
PresheafType.X [variable, in semantics.ord.presheaf]
presheaf_representables [lemma, in semantics.ord.presheaf]
presheaf_impE [lemma, in semantics.ord.presheaf]
presheaf_allEc [lemma, in semantics.ord.presheaf]
presheaf_exEc [lemma, in semantics.ord.presheaf]
presheaf_allE [lemma, in semantics.ord.presheaf]
presheaf_exE [lemma, in semantics.ord.presheaf]
presheaf_meetE [lemma, in semantics.ord.presheaf]
presheaf_joinE [lemma, in semantics.ord.presheaf]
presheaf_topE [lemma, in semantics.ord.presheaf]
presheaf_botE [lemma, in semantics.ord.presheaf]
presheaf_leE [lemma, in semantics.ord.presheaf]
presheaf_of [definition, in semantics.ord.presheaf]
presheaf_type [definition, in semantics.ord.presheaf]
presheaf_of_imp [lemma, in semantics.ord.sheaf]
presheaf_of_sheaf_monotone [instance, in semantics.ord.sheaf]
presheaf_of_sheaf [projection, in semantics.ord.sheaf]
Pro [module, in semantics.ord.protype]
prod [constructor, in semantics.ccomega.syntax]
prod [library]
ProdCLat [section, in semantics.ord.prod]
ProdCLat.T [variable, in semantics.ord.prod]
ProdCLat.X [variable, in semantics.ord.prod]
prod_pointwise_subrelation [instance, in semantics.ord.prod]
prod_impE [lemma, in semantics.ord.prod]
prod_allE [lemma, in semantics.ord.prod]
prod_exE [lemma, in semantics.ord.prod]
prod_meetE [lemma, in semantics.ord.prod]
prod_joinE [lemma, in semantics.ord.prod]
prod_botE [lemma, in semantics.ord.prod]
prod_topE [lemma, in semantics.ord.prod]
prod_leE [lemma, in semantics.ord.prod]
prod_is_prop [lemma, in semantics.base.fext]
prod_exEc [lemma, in semantics.tower.ex_similarity]
prop [constructor, in semantics.ccomega.sorts]
prop [library]
propagation [lemma, in semantics.ccomega.subjectreduction]
properties [library]
proper_monotone [instance, in semantics.ord.mono]
PropInitial [section, in semantics.ord.prop]
PropInitial.f [variable, in semantics.ord.prop]
PropInitial.X [variable, in semantics.ord.prop]
PropOrder [section, in semantics.ord.prop]
prop_initial [lemma, in semantics.ord.prop]
prop_impl_subrelation [instance, in semantics.ord.prop]
prop_impE [lemma, in semantics.ord.prop]
prop_frameP [lemma, in semantics.ord.prop]
prop_allEc [lemma, in semantics.ord.prop]
prop_exEc [lemma, in semantics.ord.prop]
prop_allE [lemma, in semantics.ord.prop]
prop_exE [lemma, in semantics.ord.prop]
prop_meetE [lemma, in semantics.ord.prop]
prop_joinE [lemma, in semantics.ord.prop]
prop_botE [lemma, in semantics.ord.prop]
prop_topE [lemma, in semantics.ord.prop]
prop_infP [lemma, in semantics.ord.prop]
prop_inf [definition, in semantics.ord.prop]
prop_le_eq [lemma, in semantics.ord.prop]
prop_leE [lemma, in semantics.ord.prop]
prop_le_trans [lemma, in semantics.ord.prop]
prop_le_refl [lemma, in semantics.ord.prop]
prop_le [definition, in semantics.ord.prop]
prop_equiv [definition, in semantics.base.overture]
prop_is_equiv [definition, in semantics.base.overture]
protype [library]
Pro.class [definition, in semantics.ord.protype]
Pro.ClassDef [section, in semantics.ord.protype]
Pro.ClassDef.cT [variable, in semantics.ord.protype]
Pro.ClassDef.T [variable, in semantics.ord.protype]
Pro.class_of [abbreviation, in semantics.ord.protype]
Pro.clone [definition, in semantics.ord.protype]
Pro.Exports [module, in semantics.ord.protype]
Pro.Exports.ProMixin [abbreviation, in semantics.ord.protype]
Pro.Exports.ProType [abbreviation, in semantics.ord.protype]
Pro.Exports.proType [abbreviation, in semantics.ord.protype]
[ proType of _ ] (form_scope) [notation, in semantics.ord.protype]
[ proType of _ for _ ] (form_scope) [notation, in semantics.ord.protype]
[ proMixin of _ ] (form_scope) [notation, in semantics.ord.protype]
Pro.Mixin [constructor, in semantics.ord.protype]
Pro.mixin_of [record, in semantics.ord.protype]
Pro.pack [definition, in semantics.ord.protype]
Pro.Pack [constructor, in semantics.ord.protype]
Pro.rel [projection, in semantics.ord.protype]
Pro.sort [projection, in semantics.ord.protype]
Pro.type [record, in semantics.ord.protype]
psstep [definition, in semantics.ccomega.churchrosser]
psstep_up [lemma, in semantics.ccomega.churchrosser]
pstep [inductive, in semantics.ccomega.churchrosser]
pstep_compat_beta [lemma, in semantics.ccomega.churchrosser]
pstep_compat [lemma, in semantics.ccomega.churchrosser]
pstep_subst [lemma, in semantics.ccomega.churchrosser]
pstep_red [lemma, in semantics.ccomega.churchrosser]
pstep_refl [lemma, in semantics.ccomega.churchrosser]
pstep_prod [constructor, in semantics.ccomega.churchrosser]
pstep_lam [constructor, in semantics.ccomega.churchrosser]
pstep_app [constructor, in semantics.ccomega.churchrosser]
pstep_sort [constructor, in semantics.ccomega.churchrosser]
pstep_var [constructor, in semantics.ccomega.churchrosser]
pstep_beta [constructor, in semantics.ccomega.churchrosser]
pt [definition, in semantics.wp.gcsemantics]
ptn [definition, in semantics.wp.icsemantics]
ptrans [definition, in semantics.wp.abstract]
pure [definition, in semantics.ord.prop]
pureA [lemma, in semantics.ord.prop]
pureB [lemma, in semantics.ord.prop]
pureE [lemma, in semantics.ord.prop]
pureH [lemma, in semantics.ord.prop]
pureI [lemma, in semantics.ord.prop]
pureJ [lemma, in semantics.ord.prop]
pureM [lemma, in semantics.ord.prop]
PurePropositions [section, in semantics.ord.prop]
PurePropositions.T [variable, in semantics.ord.prop]
⌈ _ ⌉ (ord_scope) [notation, in semantics.ord.prop]
pureS [lemma, in semantics.ord.prop]
pureT [lemma, in semantics.ord.prop]
pure_sup [lemma, in semantics.ord.prop]
pure_inf [lemma, in semantics.ord.prop]
pure_is_continuous [instance, in semantics.ord.prop]
pure_is_adjunction [instance, in semantics.ord.prop]
pure_eq [lemma, in semantics.ord.prop]
Q
quot [definition, in semantics.base.quotient]quotient [library]
QuotientMappingProperty [section, in semantics.base.quotient]
QuotientMappingProperty.A [variable, in semantics.base.quotient]
QuotientMappingProperty.B [variable, in semantics.base.quotient]
QuotientMappingProperty.R [variable, in semantics.base.quotient]
QuotientTypes [section, in semantics.base.quotient]
QuotientTypes.A [variable, in semantics.base.quotient]
QuotientTypes.Induction [section, in semantics.base.quotient]
QuotientTypes.Induction.f [variable, in semantics.base.quotient]
QuotientTypes.Induction.fP [variable, in semantics.base.quotient]
QuotientTypes.Induction.P [variable, in semantics.base.quotient]
QuotientTypes.Paths [section, in semantics.base.quotient]
QuotientTypes.R [variable, in semantics.base.quotient]
quot_map_is_equiv [definition, in semantics.base.quotient]
quot_map_retr [lemma, in semantics.base.quotient]
quot_map_sect [lemma, in semantics.base.quotient]
quot_map [definition, in semantics.base.quotient]
quot_rec2 [definition, in semantics.base.quotient]
quot_ind [definition, in semantics.base.quotient]
quot_rectE [lemma, in semantics.base.quotient]
quot_rect [definition, in semantics.base.quotient]
quot_rect_total_id [definition, in semantics.base.quotient]
quot_rect_total [definition, in semantics.base.quotient]
quot_rec [definition, in semantics.base.quotient]
R
R [inductive, in semantics.f.strongnorm]radj_of_cont [projection, in semantics.ord.cont]
rbind [definition, in semantics.ccs.syntax]
rbindA [lemma, in semantics.ccs.syntax]
rbind_rmap_comp [lemma, in semantics.ccs.syntax]
rbisim [abbreviation, in semantics.tower.ex_streams]
rbisim_equivalence [lemma, in semantics.tower.ex_streams]
rbisim_refl [lemma, in semantics.tower.ex_streams]
rcomp [definition, in semantics.ccs.syntax]
rcompA [lemma, in semantics.ccs.syntax]
rcomp_id [lemma, in semantics.ccs.syntax]
reals [library]
red [abbreviation, in semantics.ccomega.reduction]
red [inductive, in semantics.f.fcbvreduction]
RedProdSpec [inductive, in semantics.ccomega.churchrosser]
RedProdSpecI [constructor, in semantics.ccomega.churchrosser]
reducible [definition, in semantics.ars]
reduction [library]
reduction [library]
red_compat [lemma, in semantics.ccomega.reduction]
red_subst [lemma, in semantics.ccomega.reduction]
red_prod [lemma, in semantics.ccomega.reduction]
red_lam [lemma, in semantics.ccomega.reduction]
red_app [lemma, in semantics.ccomega.reduction]
red_prod_inv [lemma, in semantics.ccomega.churchrosser]
red_tapp [constructor, in semantics.f.fcbvreduction]
red_app [constructor, in semantics.f.fcbvreduction]
red_val [constructor, in semantics.f.fcbvreduction]
reflexive [definition, in semantics.base.overture]
Rel [definition, in semantics.base.overture]
ren [abbreviation, in semantics.ccs.syntax]
ren [definition, in semantics.data.fintype]
rename [definition, in semantics.f.fsyntax]
rename [definition, in semantics.debruijn.syntax]
rename [definition, in semantics.ccomega.syntax]
ren_compat [definition, in semantics.wp.icsemantics]
ren_comp [lemma, in semantics.f.fsyntax]
ren_inst_comp [lemma, in semantics.f.fsyntax]
ren_inst [lemma, in semantics.f.fsyntax]
ren_id [lemma, in semantics.f.fsyntax]
ren_comp [lemma, in semantics.debruijn.syntax]
ren_inst_comp [lemma, in semantics.debruijn.syntax]
ren_id [lemma, in semantics.debruijn.syntax]
ren_inst [lemma, in semantics.debruijn.syntax]
ren_comp [lemma, in semantics.ccomega.syntax]
ren_inst_comp [lemma, in semantics.ccomega.syntax]
ren_inst [lemma, in semantics.ccomega.syntax]
ren_id [lemma, in semantics.ccomega.syntax]
repr [definition, in semantics.base.quotient]
reprP [lemma, in semantics.base.quotient]
repr_equiv [lemma, in semantics.base.quotient]
repr_conv [lemma, in semantics.base.quotient]
repr_surjective [lemma, in semantics.base.quotient]
respectful [definition, in semantics.tower.tower]
restrict [definition, in semantics.ord.sheaf]
restrictE [lemma, in semantics.ord.sheaf]
restrictP [lemma, in semantics.ord.sheaf]
restrict_restrict [lemma, in semantics.ord.sheaf]
restrict_top [lemma, in semantics.ord.sheaf]
restrict_refl [lemma, in semantics.ord.sheaf]
reverse [definition, in semantics.ord.protype]
ReverseCLat [section, in semantics.ord.clat]
ReverseCLat.X [variable, in semantics.ord.clat]
ReverseOrder [section, in semantics.ord.ordtype]
ReverseOrder.T [variable, in semantics.ord.ordtype]
ReversePreorder [section, in semantics.ord.protype]
ReversePreorder.T [variable, in semantics.ord.protype]
reverse_le_eq [lemma, in semantics.ord.ordtype]
reverse_le_trans [lemma, in semantics.ord.protype]
reverse_le_refl [lemma, in semantics.ord.protype]
rev_leE [lemma, in semantics.ord.protype]
rev_le [definition, in semantics.ord.protype]
rev_exEc [lemma, in semantics.ord.clat]
rev_exE [lemma, in semantics.ord.clat]
rev_allEc [lemma, in semantics.ord.clat]
rev_allE [lemma, in semantics.ord.clat]
rev_infP [lemma, in semantics.ord.clat]
rev_inf [definition, in semantics.ord.clat]
rev_lfp [lemma, in semantics.tower.direct_induction]
rev_is_adjunction [instance, in semantics.ord.adj]
rho [definition, in semantics.ccomega.churchrosser]
rho_triangle [lemma, in semantics.ccomega.churchrosser]
RI [constructor, in semantics.f.strongnorm]
RightAdjoints [section, in semantics.ord.adj]
RightAdjoints.Xr [variable, in semantics.ord.adj]
RightAdjoints.Yr [variable, in semantics.ord.adj]
right_adjoint_proj [definition, in semantics.ord.adj]
rinst [definition, in semantics.wp.ic]
rinst_compF [lemma, in semantics.wp.ic]
rinst_comp [lemma, in semantics.wp.ic]
rinst_inst_comp [lemma, in semantics.wp.ic]
rinst_id [lemma, in semantics.wp.ic]
rinst_inst [lemma, in semantics.wp.ic]
rmap [definition, in semantics.ccs.syntax]
rmap_rbind_comp [lemma, in semantics.ccs.syntax]
rmap_comp [lemma, in semantics.ccs.syntax]
Rules [section, in semantics.ord.clat]
Rules.T [variable, in semantics.ord.clat]
R_rename [lemma, in semantics.f.strongnorm]
R_var [lemma, in semantics.f.strongnorm]
R_step [lemma, in semantics.f.strongnorm]
R_sn [lemma, in semantics.f.strongnorm]
S
SA [definition, in semantics.tower.ex_streams]sceil [definition, in semantics.ccs.bisim]
sceil_mono [instance, in semantics.ccs.bisim]
scomp_assoc [lemma, in semantics.debruijn.syntax]
scomp_id [lemma, in semantics.debruijn.syntax]
scomp_id_l [lemma, in semantics.debruijn.syntax]
scons [definition, in semantics.data.fintype]
scons_scomp [lemma, in semantics.ccs.syntax]
scons_scomp_eta [lemma, in semantics.debruijn.syntax]
scons_inst_eta_id [lemma, in semantics.debruijn.syntax]
scons_inst_eta [lemma, in semantics.debruijn.syntax]
scons_comp [lemma, in semantics.data.fintype]
scons_eta_id [lemma, in semantics.data.fintype]
scons_eta [lemma, in semantics.data.fintype]
sconv [definition, in semantics.ccomega.reduction]
sconv_up [lemma, in semantics.ccomega.reduction]
semantics [library]
Seq [constructor, in semantics.wp.gc]
sheaf [record, in semantics.ord.sheaf]
sheaf [library]
SheafCLat [section, in semantics.ord.sheaf]
SheafCLat.cov [variable, in semantics.ord.sheaf]
SheafCLat.X [variable, in semantics.ord.sheaf]
SheafFrame [section, in semantics.ord.sheaf]
SheafFrame.cov [variable, in semantics.ord.sheaf]
SheafFrame.X [variable, in semantics.ord.sheaf]
sheafify [definition, in semantics.ord.sheaf]
sheafifyB [lemma, in semantics.ord.sheaf]
sheafifyE [lemma, in semantics.ord.sheaf]
sheafifyEc [lemma, in semantics.ord.sheaf]
sheafifyJ [lemma, in semantics.ord.sheaf]
sheafifyM [lemma, in semantics.ord.sheaf]
sheafifyT [lemma, in semantics.ord.sheaf]
sheafify_def [lemma, in semantics.ord.sheaf]
sheafify_is_continuous [instance, in semantics.ord.sheaf]
sheafify_strong [lemma, in semantics.ord.sheaf]
sheafify_imp_ideal [lemma, in semantics.ord.sheaf]
sheafify_adj_frame [instance, in semantics.ord.sheaf]
sheafify_is_sheaf [lemma, in semantics.ord.sheaf]
sheafify_idem [lemma, in semantics.ord.sheaf]
sheafify_inc [lemma, in semantics.ord.sheaf]
sheafify_adj [instance, in semantics.ord.sheaf]
sheafP [lemma, in semantics.ord.sheaf]
sheaf_pureE [lemma, in semantics.ord.sheaf]
sheaf_exEc [lemma, in semantics.ord.sheaf]
sheaf_exE [lemma, in semantics.ord.sheaf]
sheaf_joinE [lemma, in semantics.ord.sheaf]
sheaf_botE [lemma, in semantics.ord.sheaf]
sheaf_coverageP [lemma, in semantics.ord.sheaf]
sheaf_impE [lemma, in semantics.ord.sheaf]
sheaf_frameP [lemma, in semantics.ord.sheaf]
sheaf_impP [lemma, in semantics.ord.sheaf]
sheaf_imp [definition, in semantics.ord.sheaf]
sheaf_representables [lemma, in semantics.ord.sheaf]
sheaf_exIc [lemma, in semantics.ord.sheaf]
sheaf_exI [lemma, in semantics.ord.sheaf]
sheaf_joinI [lemma, in semantics.ord.sheaf]
sheaf_exc_sheafify [lemma, in semantics.ord.sheaf]
sheaf_ex_sheafify [lemma, in semantics.ord.sheaf]
sheaf_join_sheafify [lemma, in semantics.ord.sheaf]
sheaf_bot_sheafify [lemma, in semantics.ord.sheaf]
sheaf_meetE [lemma, in semantics.ord.sheaf]
sheaf_topE [lemma, in semantics.ord.sheaf]
sheaf_allEc [lemma, in semantics.ord.sheaf]
sheaf_allE [lemma, in semantics.ord.sheaf]
sheaf_infP [lemma, in semantics.ord.sheaf]
sheaf_inf [definition, in semantics.ord.sheaf]
sheaf_leE [lemma, in semantics.ord.sheaf]
sheaf_eq [lemma, in semantics.ord.sheaf]
shelve_monotone [instance, in semantics.ord.mono]
shift [definition, in semantics.data.fintype]
shift_scons [lemma, in semantics.ccs.syntax]
shift_up [lemma, in semantics.data.fintype]
sieve [record, in semantics.ord.sheaf]
sievefun [projection, in semantics.ord.sheaf]
sieveP [lemma, in semantics.ord.sheaf]
sieve_bot [definition, in semantics.ord.sheaf]
sieve_top [definition, in semantics.ord.sheaf]
sieve_eq [lemma, in semantics.ord.sheaf]
sigT_is_hprop [lemma, in semantics.base.overture]
sigT_eq_pr2 [definition, in semantics.base.overture]
sigT_eq_pr1 [definition, in semantics.base.overture]
sigT_eq [lemma, in semantics.base.overture]
sigT_injective [lemma, in semantics.base.pext]
sig_is_hprop [lemma, in semantics.base.pext]
sig_eq [lemma, in semantics.base.pext]
sim [definition, in semantics.tower.ex_similarity]
similar [definition, in semantics.tower.ex_similarity]
Similarity [section, in semantics.tower.ex_similarity]
Similarity.A [variable, in semantics.tower.ex_similarity]
Similarity.B [variable, in semantics.tower.ex_similarity]
Similarity.Σ [variable, in semantics.tower.ex_similarity]
similar_def [lemma, in semantics.tower.ex_similarity]
simple [definition, in semantics.wp.compiler]
Skip [constructor, in semantics.wp.gc]
sn [inductive, in semantics.ars]
SNI [constructor, in semantics.ars]
sn_wn [lemma, in semantics.ars]
sn_preimage [lemma, in semantics.ars]
sort [inductive, in semantics.ccomega.sorts]
sorts [library]
sort_succ [definition, in semantics.ccomega.sorts]
sort_prod_proper [instance, in semantics.ccomega.sorts]
sort_le_typeE [lemma, in semantics.ccomega.sorts]
sort_prod [definition, in semantics.ccomega.sorts]
sort_le_eq [lemma, in semantics.ccomega.sorts]
sort_le_trans [lemma, in semantics.ccomega.sorts]
sort_le_refl [lemma, in semantics.ccomega.sorts]
sort_le [definition, in semantics.ccomega.sorts]
sound_up_to [definition, in semantics.tower.parameterized]
sred [definition, in semantics.ccomega.reduction]
sred_up [lemma, in semantics.ccomega.reduction]
star [inductive, in semantics.ars]
starES [lemma, in semantics.ars]
starR [constructor, in semantics.ars]
starSE [constructor, in semantics.ars]
star_interpolation [lemma, in semantics.ars]
star_monotone [lemma, in semantics.ars]
star_closure [lemma, in semantics.ars]
star_hom [lemma, in semantics.ars]
star_img [lemma, in semantics.ars]
star_conv [lemma, in semantics.ars]
star_trans [lemma, in semantics.ars]
star1 [lemma, in semantics.ars]
state [axiom, in semantics.wp.states]
states [library]
step [inductive, in semantics.debruijn.reduction]
step [inductive, in semantics.ccomega.reduction]
step [inductive, in semantics.ccs.semantics]
step [inductive, in semantics.f.fsemantics]
step [inductive, in semantics.wp.icsemantics]
step [projection, in semantics.tower.ex_similarity]
step_lam [constructor, in semantics.debruijn.reduction]
step_appR [constructor, in semantics.debruijn.reduction]
step_appL [constructor, in semantics.debruijn.reduction]
step_eta [constructor, in semantics.debruijn.reduction]
step_beta [constructor, in semantics.debruijn.reduction]
step_subst [lemma, in semantics.ccomega.reduction]
step_prodR [constructor, in semantics.ccomega.reduction]
step_prodL [constructor, in semantics.ccomega.reduction]
step_lam [constructor, in semantics.ccomega.reduction]
step_appR [constructor, in semantics.ccomega.reduction]
step_appL [constructor, in semantics.ccomega.reduction]
step_beta [constructor, in semantics.ccomega.reduction]
step_fix_inv [lemma, in semantics.ccs.semantics]
step_new_inv [lemma, in semantics.ccs.semantics]
step_par_inv [lemma, in semantics.ccs.semantics]
step_sum_inv [lemma, in semantics.ccs.semantics]
step_act_inv [lemma, in semantics.ccs.semantics]
step_fix [constructor, in semantics.ccs.semantics]
step_restrict [constructor, in semantics.ccs.semantics]
step_comm [constructor, in semantics.ccs.semantics]
step_parr [constructor, in semantics.ccs.semantics]
step_parl [constructor, in semantics.ccs.semantics]
step_sumr [constructor, in semantics.ccs.semantics]
step_suml [constructor, in semantics.ccs.semantics]
step_act [constructor, in semantics.ccs.semantics]
step_pstep [lemma, in semantics.ccomega.churchrosser]
step_inst [lemma, in semantics.f.fsemantics]
step_weak [lemma, in semantics.f.fsemantics]
step_tlam [constructor, in semantics.f.fsemantics]
step_lam [constructor, in semantics.f.fsemantics]
step_appR [constructor, in semantics.f.fsemantics]
step_appL [constructor, in semantics.f.fsemantics]
step_tbeta [constructor, in semantics.f.fsemantics]
step_beta [constructor, in semantics.f.fsemantics]
step_if_false [constructor, in semantics.wp.icsemantics]
step_if_true [constructor, in semantics.wp.icsemantics]
step_def [constructor, in semantics.wp.icsemantics]
step_act [constructor, in semantics.wp.icsemantics]
Streams [section, in semantics.tower.ex_streams]
Streams.A [variable, in semantics.tower.ex_streams]
stream_companionP [lemma, in semantics.tower.ex_streams]
stream_companion [definition, in semantics.tower.ex_streams]
strongnorm [library]
strong_normalization [lemma, in semantics.f.strongnorm]
sub [inductive, in semantics.ccomega.subtyping]
SubcanonicalCoverage [section, in semantics.ord.sheaf]
SubcanonicalCoverageOrd [section, in semantics.ord.sheaf]
SubcanonicalCoverageOrd.b [variable, in semantics.ord.sheaf]
SubcanonicalCoverageOrd.X [variable, in semantics.ord.sheaf]
SubcanonicalCoverage.b [variable, in semantics.ord.sheaf]
SubcanonicalCoverage.X [variable, in semantics.ord.sheaf]
subcanonical_embedE [lemma, in semantics.ord.sheaf]
SubI [constructor, in semantics.ccomega.subtyping]
subjectreduction [library]
subject_reduction [lemma, in semantics.ccomega.subjectreduction]
subst [definition, in semantics.wp.ic]
subst [definition, in semantics.f.fsyntax]
subst [definition, in semantics.debruijn.syntax]
subst [definition, in semantics.ccomega.syntax]
substitutivity [lemma, in semantics.debruijn.reduction]
subst_up [lemma, in semantics.ccs.syntax]
subst_extend [lemma, in semantics.ccs.syntax]
subtyping [library]
sub_inst [lemma, in semantics.ccomega.subtyping]
sub_prod_inv [lemma, in semantics.ccomega.subtyping]
sub_trans [lemma, in semantics.ccomega.subtyping]
sub_sort [lemma, in semantics.ccomega.subtyping]
sub_refl [lemma, in semantics.ccomega.subtyping]
sub1 [inductive, in semantics.ccomega.subtyping]
sub1_inst [lemma, in semantics.ccomega.subtyping]
sub1_trans [lemma, in semantics.ccomega.subtyping]
sub1_conv [lemma, in semantics.ccomega.subtyping]
sub1_sub [lemma, in semantics.ccomega.subtyping]
sub1_prod [constructor, in semantics.ccomega.subtyping]
sub1_sort [constructor, in semantics.ccomega.subtyping]
sub1_refl [constructor, in semantics.ccomega.subtyping]
Sum [constructor, in semantics.ccs.syntax]
sum_proper [instance, in semantics.ccs.bisim]
sup [definition, in semantics.ord.clat]
supguard [definition, in semantics.ord.clat]
sup_closed_wpi_distributive [lemma, in semantics.wp.icsemantics]
sup_closed [definition, in semantics.ord.clat]
sup_closed_wp_distributive [lemma, in semantics.wp.gcsemantics]
sup_canonical [lemma, in semantics.ord.sheaf]
surjective [definition, in semantics.base.inhab]
symmetric [definition, in semantics.base.overture]
syntax [library]
syntax [library]
syntax [library]
T
t [abbreviation, in semantics.tower.parameterized]T [abbreviation, in semantics.tower.cocontinuous_tower]
T [abbreviation, in semantics.tower.linear_tower]
t [definition, in semantics.tower.tower]
T [inductive, in semantics.tower.tower]
T [abbreviation, in semantics.tower.direct_induction]
tag_injective [lemma, in semantics.base.overture]
tapp [constructor, in semantics.f.fsyntax]
tapp [constructor, in semantics.f.fcbvsyntax]
tarski [library]
TarskiGfp [section, in semantics.tower.tarski]
TarskiGfp.f [variable, in semantics.tower.tarski]
TarskiGfp.fr [variable, in semantics.tower.tarski]
TarskiGfp.X [variable, in semantics.tower.tarski]
TarskiLfp [section, in semantics.tower.tarski]
TarskiLfp.f [variable, in semantics.tower.tarski]
TarskiLfp.X [variable, in semantics.tower.tarski]
terminates [definition, in semantics.wp.icsemantics]
terminates_def [lemma, in semantics.wp.icsemantics]
Termination [section, in semantics.ars]
Termination.cr [variable, in semantics.ars]
Termination.e [variable, in semantics.ars]
Termination.T [variable, in semantics.ars]
tlam [constructor, in semantics.f.fsyntax]
tlam [constructor, in semantics.f.fcbvsyntax]
tm [inductive, in semantics.wp.ic]
tm [inductive, in semantics.f.fsyntax]
tm [inductive, in semantics.debruijn.syntax]
tm [inductive, in semantics.ccomega.syntax]
tm [inductive, in semantics.f.fcbvsyntax]
Tm_has_type [definition, in semantics.f.weaknorm]
tm_has_type_ind [definition, in semantics.f.weaknorm]
tm_has_type [inductive, in semantics.f.weaknorm]
tm_inst_comp [lemma, in semantics.f.fcbvsyntax]
tm_inst_ren_comp [lemma, in semantics.f.fcbvsyntax]
tm_ren_comp [lemma, in semantics.f.fcbvsyntax]
tm_ren_inst_comp [lemma, in semantics.f.fcbvsyntax]
tm_inst_ids [lemma, in semantics.f.fcbvsyntax]
tm_ren_inst [lemma, in semantics.f.fcbvsyntax]
tm_ren_id [lemma, in semantics.f.fcbvsyntax]
tm_inst [definition, in semantics.f.fcbvsyntax]
tm_rename [definition, in semantics.f.fcbvsyntax]
tm_ind [definition, in semantics.f.fcbvsyntax]
top [definition, in semantics.ord.clat]
topI [lemma, in semantics.ord.clat]
top_def [lemma, in semantics.ord.clat]
top_eq [lemma, in semantics.ord.clat]
Tower [section, in semantics.tower.tower]
tower [library]
TowerCompanion [section, in semantics.tower.cocontinuous_tower]
TowerCompanion.f [variable, in semantics.tower.cocontinuous_tower]
TowerCompanion.f_cocontinuous [variable, in semantics.tower.cocontinuous_tower]
TowerCompanion.f_mono [variable, in semantics.tower.cocontinuous_tower]
TowerCompanion.X [variable, in semantics.tower.cocontinuous_tower]
tower_wf [lemma, in semantics.tower.linear_tower]
tower_linear [lemma, in semantics.tower.linear_tower]
tower_linear_right [lemma, in semantics.tower.linear_tower]
tower_linear_left [lemma, in semantics.tower.linear_tower]
tower_f_linear [lemma, in semantics.tower.linear_tower]
tower_induction [lemma, in semantics.tower.tower]
tower_dec [lemma, in semantics.tower.tower]
Tower.DoubleInd [section, in semantics.tower.tower]
Tower.DoubleInd.limit [variable, in semantics.tower.tower]
Tower.DoubleInd.R [variable, in semantics.tower.tower]
Tower.DoubleInd.step [variable, in semantics.tower.tower]
Tower.f [variable, in semantics.tower.tower]
Tower.f_mono [variable, in semantics.tower.tower]
Tower.UptoLemma [section, in semantics.tower.tower]
Tower.UptoLemmaCharacterization [section, in semantics.tower.tower]
Tower.UptoLemmaCharacterization.tt [variable, in semantics.tower.tower]
Tower.UptoLemmaCharacterization.upto [variable, in semantics.tower.tower]
Tower.UptoLemma.g [variable, in semantics.tower.tower]
Tower.UptoLemma.g_mono [variable, in semantics.tower.tower]
Tower.X [variable, in semantics.tower.tower]
tpred [definition, in semantics.f.strongnorm]
transitive [definition, in semantics.base.overture]
transport [definition, in semantics.base.overture]
transport_const [lemma, in semantics.base.overture]
triangle [definition, in semantics.ars]
triangle_cofinal [lemma, in semantics.ars]
triangle_monotone [lemma, in semantics.ars]
triangle_diamond [lemma, in semantics.ars]
triple [definition, in semantics.wp.gcsemantics]
tripleG [definition, in semantics.wp.gcsemantics]
TruncationMappingProperty [section, in semantics.base.fext]
TruncationMappingProperty.A [variable, in semantics.base.fext]
TruncationMappingProperty.B [variable, in semantics.base.fext]
tup [definition, in semantics.f.types]
tup_ids [lemma, in semantics.f.types]
tvar [constructor, in semantics.f.types]
tv_inst_comp [lemma, in semantics.f.fcbvsyntax]
tv_inst_ren_comp [lemma, in semantics.f.fcbvsyntax]
tv_ren_inst_comp [lemma, in semantics.f.fcbvsyntax]
tv_ren_inst [lemma, in semantics.f.fcbvsyntax]
tv_ren_id [lemma, in semantics.f.fcbvsyntax]
tv_ind [definition, in semantics.f.fcbvsyntax]
ty [inductive, in semantics.f.types]
tyinst [definition, in semantics.f.types]
type [constructor, in semantics.ccomega.sorts]
types [library]
typing [library]
tyrename [definition, in semantics.f.types]
tysubst [definition, in semantics.f.types]
tysubst_upi [lemma, in semantics.ccomega.contextmorphism]
tysubst_up [lemma, in semantics.ccomega.contextmorphism]
tysubst_cons [lemma, in semantics.ccomega.contextmorphism]
tysubst_shift [lemma, in semantics.ccomega.contextmorphism]
tysubst_ren_comp [lemma, in semantics.ccomega.contextmorphism]
tysubst_comp [lemma, in semantics.ccomega.contextmorphism]
tysubst_var [lemma, in semantics.ccomega.contextmorphism]
tysubst_ids [lemma, in semantics.ccomega.contextmorphism]
ty_tlam [constructor, in semantics.f.weaknorm]
ty_lam [constructor, in semantics.f.weaknorm]
ty_var [constructor, in semantics.f.weaknorm]
ty_tapp [constructor, in semantics.f.weaknorm]
ty_app [constructor, in semantics.f.weaknorm]
ty_val [constructor, in semantics.f.weaknorm]
ty_tlam [constructor, in semantics.f.fsemantics]
ty_tapp [constructor, in semantics.f.fsemantics]
ty_lam [constructor, in semantics.f.fsemantics]
ty_app [constructor, in semantics.f.fsemantics]
ty_var [constructor, in semantics.f.fsemantics]
ty_prod_wf [lemma, in semantics.ccomega.typing]
ty_sort_wf [lemma, in semantics.ccomega.typing]
ty_eapp [lemma, in semantics.ccomega.typing]
ty_sub [constructor, in semantics.ccomega.typing]
ty_prod [constructor, in semantics.ccomega.typing]
ty_lam [constructor, in semantics.ccomega.typing]
ty_app [constructor, in semantics.ccomega.typing]
ty_sort [constructor, in semantics.ccomega.typing]
ty_var [constructor, in semantics.ccomega.typing]
ty_scomp_assoc [lemma, in semantics.f.types]
ty_inst_comp [lemma, in semantics.f.types]
ty_tup_comp [lemma, in semantics.f.types]
ty_inst_ren_comp [lemma, in semantics.f.types]
ty_tup_up_comp [lemma, in semantics.f.types]
ty_ren_comp [lemma, in semantics.f.types]
ty_ren_inst_comp [lemma, in semantics.f.types]
ty_scomp_idR [lemma, in semantics.f.types]
ty_inst_ids [lemma, in semantics.f.types]
ty_ren_id [lemma, in semantics.f.types]
ty_ren_inst [lemma, in semantics.f.types]
ty_ctx_conv [lemma, in semantics.ccomega.contextmorphism]
ty_cut [lemma, in semantics.ccomega.contextmorphism]
ty_subst [lemma, in semantics.ccomega.contextmorphism]
ty_map [lemma, in semantics.ccomega.contextmorphism]
ty_lam_inv [lemma, in semantics.ccomega.subjectreduction]
ty_lam_invX [lemma, in semantics.ccomega.subjectreduction]
ty_prod_inv [lemma, in semantics.ccomega.subjectreduction]
ty_prod_invX [lemma, in semantics.ccomega.subjectreduction]
T_kleene [lemma, in semantics.tower.cocontinuous_tower]
T_iter [lemma, in semantics.tower.cocontinuous_tower]
t_greatest_respectful [lemma, in semantics.tower.tower]
t_greatest_compatible [lemma, in semantics.tower.tower]
t_compat [lemma, in semantics.tower.tower]
t_fdec [lemma, in semantics.tower.tower]
t_gfp [lemma, in semantics.tower.tower]
t_f [lemma, in semantics.tower.tower]
t_img [lemma, in semantics.tower.tower]
t_idem [lemma, in semantics.tower.tower]
t_inc [lemma, in semantics.tower.tower]
t_monotone [instance, in semantics.tower.tower]
t_closure [instance, in semantics.tower.tower]
T_t [lemma, in semantics.tower.tower]
T_ind2 [lemma, in semantics.tower.tower]
T_lim [constructor, in semantics.tower.tower]
T_step [constructor, in semantics.tower.tower]
T_C [lemma, in semantics.tower.direct_induction]
T_dec [lemma, in semantics.tower.direct_induction]
T_gfp [lemma, in semantics.tower.direct_induction]
U
ubP [lemma, in semantics.ord.protype]unembed [definition, in semantics.ord.sheaf]
unembed_embed [lemma, in semantics.ord.sheaf]
unify [definition, in semantics.base.meta]
unique_solutions1 [lemma, in semantics.ccs.properties]
unique_solutions [lemma, in semantics.ccs.properties]
unit_is_hprop [lemma, in semantics.base.overture]
univ [constructor, in semantics.ccomega.syntax]
up [definition, in semantics.data.fintype]
upE [lemma, in semantics.ccs.syntax]
upi [definition, in semantics.wp.ic]
upi [definition, in semantics.ccs.syntax]
upi [definition, in semantics.f.fsyntax]
upi [definition, in semantics.debruijn.syntax]
upi [definition, in semantics.ccomega.syntax]
upi_comp [lemma, in semantics.wp.ic]
upi_comp [lemma, in semantics.f.fsyntax]
upi_up_comp [lemma, in semantics.f.fsyntax]
upi_ids [lemma, in semantics.f.fsyntax]
upi_comp [lemma, in semantics.debruijn.syntax]
upi_up_comp [lemma, in semantics.debruijn.syntax]
upi_ids [lemma, in semantics.debruijn.syntax]
upi_def [lemma, in semantics.debruijn.syntax]
upi_comp [lemma, in semantics.ccomega.syntax]
upi_up_comp [lemma, in semantics.ccomega.syntax]
upi_ids [lemma, in semantics.ccomega.syntax]
upi_ids [lemma, in semantics.f.fcbvsyntax]
upper_lopen [projection, in semantics.tower.reals]
upper_uset [projection, in semantics.tower.reals]
upper_interval [projection, in semantics.tower.reals]
upr_up [lemma, in semantics.ccs.syntax]
upto_inst [lemma, in semantics.ccs.bisim]
upto_fix_o [lemma, in semantics.ccs.bisim]
upto_fix_gen [lemma, in semantics.ccs.bisim]
upto_inst_beta' [lemma, in semantics.ccs.bisim]
upto_inst' [lemma, in semantics.ccs.bisim]
upto_new_o [lemma, in semantics.ccs.bisim]
upto_par_o [lemma, in semantics.ccs.bisim]
upto_sum_o [instance, in semantics.ccs.bisim]
upto_act_open [instance, in semantics.ccs.bisim]
upto_act [instance, in semantics.ccs.bisim]
upto_act_s_open [lemma, in semantics.ccs.bisim]
upto_act_s [lemma, in semantics.ccs.bisim]
upto_context [lemma, in semantics.tower.ex_streams]
upto_to_tower_induction [lemma, in semantics.tower.tower]
upto_lemma [lemma, in semantics.tower.tower]
up_comp [lemma, in semantics.ccs.syntax]
up_upr [lemma, in semantics.ccs.syntax]
up_ren [lemma, in semantics.ccs.syntax]
up_id [lemma, in semantics.ccs.syntax]
V
V [definition, in semantics.f.weaknorm]V [abbreviation, in semantics.f.strongnorm]
val [constructor, in semantics.f.fcbvsyntax]
Var [constructor, in semantics.ccs.syntax]
var [constructor, in semantics.f.fsyntax]
var [constructor, in semantics.debruijn.syntax]
Var [projection, in semantics.f.types]
var [constructor, in semantics.ccomega.syntax]
var [constructor, in semantics.f.fcbvsyntax]
vl [inductive, in semantics.f.fcbvsyntax]
Vl_has_type [definition, in semantics.f.weaknorm]
vl_has_type_ind [definition, in semantics.f.weaknorm]
vl_has_type [inductive, in semantics.f.weaknorm]
vl_inst_comp [lemma, in semantics.f.fcbvsyntax]
vl_inst_ren_comp [lemma, in semantics.f.fcbvsyntax]
vl_ren_comp [lemma, in semantics.f.fcbvsyntax]
vl_ren_inst_comp [lemma, in semantics.f.fcbvsyntax]
vl_inst_ids [lemma, in semantics.f.fcbvsyntax]
vl_ren_inst [lemma, in semantics.f.fcbvsyntax]
vl_ren_id [lemma, in semantics.f.fcbvsyntax]
vl_inst [definition, in semantics.f.fcbvsyntax]
vl_rename [definition, in semantics.f.fcbvsyntax]
vl_ind [definition, in semantics.f.fcbvsyntax]
vsubst [definition, in semantics.f.fcbvsyntax]
vup [definition, in semantics.f.fcbvsyntax]
vup_comp [lemma, in semantics.f.fcbvsyntax]
vup_up_comp [lemma, in semantics.f.fcbvsyntax]
V_beta [lemma, in semantics.f.weaknorm]
V_weaken [lemma, in semantics.f.weaknorm]
V_all [lemma, in semantics.f.weaknorm]
V_arr [lemma, in semantics.f.weaknorm]
V_to_E [lemma, in semantics.f.weaknorm]
V_beta [lemma, in semantics.f.strongnorm]
V_weaken [lemma, in semantics.f.strongnorm]
W
weaken [lemma, in semantics.ord.frame]weakening [lemma, in semantics.ccomega.contextmorphism]
weakly_guarded_inst [lemma, in semantics.ccs.properties]
weakly_guarded [definition, in semantics.ccs.properties]
weaknorm [library]
weak_normalization [lemma, in semantics.f.weaknorm]
wlp [definition, in semantics.wp.abstract]
wlp [definition, in semantics.wp.gcsemantics]
wlpi [definition, in semantics.wp.icsemantics]
wlpi_compile_correct [lemma, in semantics.wp.compiler]
wlpi_comp [lemma, in semantics.wp.compiler]
wlpi_flatmapF [lemma, in semantics.wp.compiler]
wlpi_flatmapT [lemma, in semantics.wp.compiler]
wlpi_flatmap [lemma, in semantics.wp.compiler]
wlpi_let [lemma, in semantics.wp.compiler]
wlpi_eval [lemma, in semantics.wp.icsemantics]
wlpi_mstep [lemma, in semantics.wp.icsemantics]
wlpi_step [lemma, in semantics.wp.icsemantics]
wlpi_is_distributive [lemma, in semantics.wp.icsemantics]
wlpi_distributes_over_wpi [lemma, in semantics.wp.icsemantics]
wlpi_beta [lemma, in semantics.wp.icsemantics]
wlpi_inst [lemma, in semantics.wp.icsemantics]
wlpi_weaken [lemma, in semantics.wp.icsemantics]
wlpi_ren [lemma, in semantics.wp.icsemantics]
wlpi_def [lemma, in semantics.wp.icsemantics]
wlpi_def_gfp [lemma, in semantics.wp.icsemantics]
wlpi_if [lemma, in semantics.wp.icsemantics]
wlpi_jump [lemma, in semantics.wp.icsemantics]
wlpi_act [lemma, in semantics.wp.icsemantics]
wlps [inductive, in semantics.wp.gcsemantics]
wlps_to_wlp [lemma, in semantics.wp.gcsemantics]
wlps_do [constructor, in semantics.wp.gcsemantics]
wlps_case [constructor, in semantics.wp.gcsemantics]
wlps_seq [constructor, in semantics.wp.gcsemantics]
wlps_act [constructor, in semantics.wp.gcsemantics]
wlps_skip [constructor, in semantics.wp.gcsemantics]
wlp_to_wp [lemma, in semantics.wp.abstract]
wlp_distributes_over [lemma, in semantics.wp.abstract]
wlp_distributes_over_wp [lemma, in semantics.wp.abstract]
wlp_distributive [lemma, in semantics.wp.abstract]
wlp_mono [lemma, in semantics.wp.abstract]
wlp_is_distributive [lemma, in semantics.wp.gcsemantics]
wlp_distributes_over_wp [lemma, in semantics.wp.gcsemantics]
wlp_wlps_equiv [lemma, in semantics.wp.gcsemantics]
wlp_to_wlps [lemma, in semantics.wp.gcsemantics]
wlp_do [lemma, in semantics.wp.gcsemantics]
wlp_loop_mono [instance, in semantics.wp.gcsemantics]
wlp_loop [definition, in semantics.wp.gcsemantics]
wlp_case [lemma, in semantics.wp.gcsemantics]
wlp_seq [lemma, in semantics.wp.gcsemantics]
wlp_act [lemma, in semantics.wp.gcsemantics]
wlp_skip [lemma, in semantics.wp.gcsemantics]
wn [definition, in semantics.ars]
wn_accn [lemma, in semantics.ars]
wp [definition, in semantics.wp.abstract]
wp [definition, in semantics.wp.gcsemantics]
wpF [definition, in semantics.wp.gcsemantics]
wpF_distributive [lemma, in semantics.wp.gcsemantics]
wpF_mono [instance, in semantics.wp.gcsemantics]
wpG [definition, in semantics.wp.gcsemantics]
wpG_mono [instance, in semantics.wp.gcsemantics]
wpG_eqn [lemma, in semantics.wp.gcsemantics]
wpi [definition, in semantics.wp.icsemantics]
wpI [definition, in semantics.wp.icsemantics]
wpi_compile_correct [lemma, in semantics.wp.compiler]
wpi_comp [lemma, in semantics.wp.compiler]
wpi_flatmapF [lemma, in semantics.wp.compiler]
wpi_flatmapT [lemma, in semantics.wp.compiler]
wpi_flatmap [lemma, in semantics.wp.compiler]
wpi_let [lemma, in semantics.wp.compiler]
wpi_operational [lemma, in semantics.wp.icsemantics]
wpi_terminates [lemma, in semantics.wp.icsemantics]
wpi_terminates_subst [lemma, in semantics.wp.icsemantics]
wpi_eval [lemma, in semantics.wp.icsemantics]
wpi_mstep [lemma, in semantics.wp.icsemantics]
wpi_step [lemma, in semantics.wp.icsemantics]
wpi_lfp_kleene [lemma, in semantics.wp.icsemantics]
wpi_Ω [lemma, in semantics.wp.icsemantics]
wpi_deterministic [lemma, in semantics.wp.icsemantics]
wpi_is_distributive [lemma, in semantics.wp.icsemantics]
wpI_distributive [lemma, in semantics.wp.icsemantics]
wpi_distributive [definition, in semantics.wp.icsemantics]
wpi_beta [lemma, in semantics.wp.icsemantics]
wpi_inst [lemma, in semantics.wp.icsemantics]
wpi_weaken [lemma, in semantics.wp.icsemantics]
wpi_ren [lemma, in semantics.wp.icsemantics]
wpI_ren_compat [lemma, in semantics.wp.icsemantics]
wpi_def [lemma, in semantics.wp.icsemantics]
wpi_def_lfp [lemma, in semantics.wp.icsemantics]
wpi_if [lemma, in semantics.wp.icsemantics]
wpi_jump [lemma, in semantics.wp.icsemantics]
wpi_act [lemma, in semantics.wp.icsemantics]
wpI_mono [instance, in semantics.wp.icsemantics]
wpn_mono [lemma, in semantics.wp.icsemantics]
wps [inductive, in semantics.wp.gcsemantics]
wps_to_wp [lemma, in semantics.wp.gcsemantics]
wps_do_false [constructor, in semantics.wp.gcsemantics]
wps_do_true [constructor, in semantics.wp.gcsemantics]
wps_case [constructor, in semantics.wp.gcsemantics]
wps_seq [constructor, in semantics.wp.gcsemantics]
wps_act [constructor, in semantics.wp.gcsemantics]
wps_skip [constructor, in semantics.wp.gcsemantics]
wp_deterministic [lemma, in semantics.wp.abstract]
wp_continuous [lemma, in semantics.wp.abstract]
wp_distributive_over [lemma, in semantics.wp.abstract]
wp_distributive [lemma, in semantics.wp.abstract]
wp_mono [lemma, in semantics.wp.abstract]
wp_to_wlp [lemma, in semantics.wp.abstract]
wp_continuous [lemma, in semantics.wp.gcsemantics]
wp_wpG_continuous [lemma, in semantics.wp.gcsemantics]
wp_is_distributive [lemma, in semantics.wp.gcsemantics]
wp_distributive [definition, in semantics.wp.gcsemantics]
wp_wps_equiv [lemma, in semantics.wp.gcsemantics]
wp_to_wps [lemma, in semantics.wp.gcsemantics]
wp_do [lemma, in semantics.wp.gcsemantics]
wp_loop_mono [instance, in semantics.wp.gcsemantics]
wp_loop [definition, in semantics.wp.gcsemantics]
wp_case [lemma, in semantics.wp.gcsemantics]
wp_seq [lemma, in semantics.wp.gcsemantics]
wp_act [lemma, in semantics.wp.gcsemantics]
wp_skip [lemma, in semantics.wp.gcsemantics]
wp_do_eqn [lemma, in semantics.wp.gcsemantics]
wp_mono [lemma, in semantics.wp.gcsemantics]
X
xi_extS [lemma, in semantics.base.fext]xi_extP [lemma, in semantics.base.fext]
xi_ext [lemma, in semantics.base.fext]
Y
yo [definition, in semantics.ord.presheaf]yoneda [lemma, in semantics.ord.presheaf]
Yoneda [section, in semantics.ord.presheaf]
YonedaClat [section, in semantics.ord.presheaf]
YonedaClat.X [variable, in semantics.ord.presheaf]
YonedaOrd [section, in semantics.ord.presheaf]
YonedaOrd.X [variable, in semantics.ord.presheaf]
Yoneda.X [variable, in semantics.ord.presheaf]
yo_meet [lemma, in semantics.ord.presheaf]
yo_top [lemma, in semantics.ord.presheaf]
yo_inf [lemma, in semantics.ord.presheaf]
yo_injective [lemma, in semantics.ord.presheaf]
yo_limit [lemma, in semantics.ord.presheaf]
yo_embedding [lemma, in semantics.ord.presheaf]
other
_ .2 (fibration_scope) [notation, in semantics.base.overture]_ .1 (fibration_scope) [notation, in semantics.base.overture]
( _ ; _ ) (fibration_scope) [notation, in semantics.base.overture]
_ → _ (ord_scope) [notation, in semantics.ord.frame]
⌈ _ ⌉ (ord_scope) [notation, in semantics.ord.prop]
_ ≤ _ :> _ (ord_scope) [notation, in semantics.ord.protype]
_ ≤ _ (ord_scope) [notation, in semantics.ord.protype]
_ ∨ _ (ord_scope) [notation, in semantics.ord.clat]
_ ∧ _ (ord_scope) [notation, in semantics.ord.clat]
⊥ (ord_scope) [notation, in semantics.ord.clat]
⊤ (ord_scope) [notation, in semantics.ord.clat]
∃ _ .. _ | _ , _ (ord_scope) [notation, in semantics.ord.clat]
∃ _ .. _ , _ (ord_scope) [notation, in semantics.ord.clat]
∀ _ .. _ | _ , _ (ord_scope) [notation, in semantics.ord.clat]
∀ _ .. _ , _ (ord_scope) [notation, in semantics.ord.clat]
_ ⊏ _ :> _ (ord_scope) [notation, in semantics.tower.llat]
_ ⊏ _ (ord_scope) [notation, in semantics.tower.llat]
_ ^* (ord_scope) [notation, in semantics.ord.adj]
_ .: _ (subst_scope) [notation, in semantics.data.fintype]
_ >> _ (subst_scope) [notation, in semantics.data.fintype]
_ ^r (type_scope) [notation, in semantics.ord.protype]
○ _ (type_scope) [notation, in semantics.ccs.bisim]
{ mono _ } (type_scope) [notation, in semantics.ord.mfun]
_ <~> _ (type_scope) [notation, in semantics.base.overture]
hexists _ .. _ , _ (type_scope) [notation, in semantics.base.inhab]
'Error: _ _ (unify_scope) [notation, in semantics.base.meta]
[find _ | _ ~ _ | _ ] _ (unify_scope) [notation, in semantics.base.meta]
[find _ | _ ~ _ ] _ (unify_scope) [notation, in semantics.base.meta]
_ === _ [notation, in semantics.ccomega.reduction]
_ <: _ [notation, in semantics.ccomega.subtyping]
_ .[ _ /] [notation, in semantics.ccs.syntax]
_ .[ _ ] [notation, in semantics.ccs.syntax]
_ >>> _ [notation, in semantics.ccs.syntax]
_ ~~ _ [notation, in semantics.ccs.bisim]
_ |- _ ~ _ [notation, in semantics.ccs.bisim]
_ ^-1 [notation, in semantics.base.overture]
_ ..2 [notation, in semantics.base.overture]
_ ..1 [notation, in semantics.base.overture]
_ # _ [notation, in semantics.base.overture]
_ ^- [notation, in semantics.tower.llat]
_ ^+ [notation, in semantics.tower.llat]
[ _ |- _ ] [notation, in semantics.ccomega.typing]
[ _ |- _ :- _ ] [notation, in semantics.ccomega.typing]
[ _ |- _ -| _ ] [notation, in semantics.ccomega.contextmorphism]
Ω [definition, in semantics.wp.ic]
ε [definition, in semantics.tower.ex_streams]
ε_cocontinuous [lemma, in semantics.tower.ex_streams]
ε_mono [instance, in semantics.tower.ex_streams]
ν [definition, in semantics.tower.gfp_companion]
Notation Index
C
[ clat of _ ] (form_scope) [in semantics.ord.clat][ clat of _ for _ ] (form_scope) [in semantics.ord.clat]
[ clatMixin of _ ] (form_scope) [in semantics.ord.clat]
F
[ frame of _ ] (form_scope) [in semantics.ord.frame][ frame of _ for _ ] (form_scope) [in semantics.ord.frame]
[ frameMixin of _ ] (form_scope) [in semantics.ord.frame]
I
_ ^- [in semantics.tower.reals]_ ^+ [in semantics.tower.reals]
L
[ llat of _ ] (form_scope) [in semantics.tower.llat][ llat of _ for _ ] (form_scope) [in semantics.tower.llat]
[ llatMixin of _ ] (form_scope) [in semantics.tower.llat]
O
[ ordType of _ ] (form_scope) [in semantics.ord.ordtype][ ordType of _ for _ ] (form_scope) [in semantics.ord.ordtype]
[ ordMixin of _ ] (form_scope) [in semantics.ord.ordtype]
P
[ proType of _ ] (form_scope) [in semantics.ord.protype][ proType of _ for _ ] (form_scope) [in semantics.ord.protype]
[ proMixin of _ ] (form_scope) [in semantics.ord.protype]
⌈ _ ⌉ (ord_scope) [in semantics.ord.prop]
other
_ .2 (fibration_scope) [in semantics.base.overture]_ .1 (fibration_scope) [in semantics.base.overture]
( _ ; _ ) (fibration_scope) [in semantics.base.overture]
_ → _ (ord_scope) [in semantics.ord.frame]
⌈ _ ⌉ (ord_scope) [in semantics.ord.prop]
_ ≤ _ :> _ (ord_scope) [in semantics.ord.protype]
_ ≤ _ (ord_scope) [in semantics.ord.protype]
_ ∨ _ (ord_scope) [in semantics.ord.clat]
_ ∧ _ (ord_scope) [in semantics.ord.clat]
⊥ (ord_scope) [in semantics.ord.clat]
⊤ (ord_scope) [in semantics.ord.clat]
∃ _ .. _ | _ , _ (ord_scope) [in semantics.ord.clat]
∃ _ .. _ , _ (ord_scope) [in semantics.ord.clat]
∀ _ .. _ | _ , _ (ord_scope) [in semantics.ord.clat]
∀ _ .. _ , _ (ord_scope) [in semantics.ord.clat]
_ ⊏ _ :> _ (ord_scope) [in semantics.tower.llat]
_ ⊏ _ (ord_scope) [in semantics.tower.llat]
_ ^* (ord_scope) [in semantics.ord.adj]
_ .: _ (subst_scope) [in semantics.data.fintype]
_ >> _ (subst_scope) [in semantics.data.fintype]
_ ^r (type_scope) [in semantics.ord.protype]
○ _ (type_scope) [in semantics.ccs.bisim]
{ mono _ } (type_scope) [in semantics.ord.mfun]
_ <~> _ (type_scope) [in semantics.base.overture]
hexists _ .. _ , _ (type_scope) [in semantics.base.inhab]
'Error: _ _ (unify_scope) [in semantics.base.meta]
[find _ | _ ~ _ | _ ] _ (unify_scope) [in semantics.base.meta]
[find _ | _ ~ _ ] _ (unify_scope) [in semantics.base.meta]
_ === _ [in semantics.ccomega.reduction]
_ <: _ [in semantics.ccomega.subtyping]
_ .[ _ /] [in semantics.ccs.syntax]
_ .[ _ ] [in semantics.ccs.syntax]
_ >>> _ [in semantics.ccs.syntax]
_ ~~ _ [in semantics.ccs.bisim]
_ |- _ ~ _ [in semantics.ccs.bisim]
_ ^-1 [in semantics.base.overture]
_ ..2 [in semantics.base.overture]
_ ..1 [in semantics.base.overture]
_ # _ [in semantics.base.overture]
_ ^- [in semantics.tower.llat]
_ ^+ [in semantics.tower.llat]
[ _ |- _ ] [in semantics.ccomega.typing]
[ _ |- _ :- _ ] [in semantics.ccomega.typing]
[ _ |- _ -| _ ] [in semantics.ccomega.contextmorphism]
Module Index
C
CLat [in semantics.ord.clat]CLat.Exports [in semantics.ord.clat]
F
Frame [in semantics.ord.frame]Frame.Exports [in semantics.ord.frame]
I
Inhab [in semantics.base.inhab]L
LLat [in semantics.tower.llat]LLat.Exports [in semantics.tower.llat]
O
Ord [in semantics.ord.ordtype]Ord.Exports [in semantics.ord.ordtype]
P
Pataraia [in semantics.tower.direct_induction]Pro [in semantics.ord.protype]
Pro.Exports [in semantics.ord.protype]
Variable Index
A
AbstractPredTrans.E [in semantics.wp.abstract]AbstractPredTrans.T [in semantics.wp.abstract]
AbstractPredTrans.X [in semantics.wp.abstract]
AbstractPredTrans.Y [in semantics.wp.abstract]
AdjunctionsCLat.f [in semantics.ord.adj]
AdjunctionsCLat.g [in semantics.ord.adj]
AdjunctionsCLat.X [in semantics.ord.adj]
AdjunctionsCLat.Y [in semantics.ord.adj]
AdjunctionsFrame.f [in semantics.ord.adj]
AdjunctionsFrame.g [in semantics.ord.adj]
AdjunctionsFrame.X [in semantics.ord.adj]
AdjunctionsFrame.Y [in semantics.ord.adj]
AdjunctionsOrdDual.X [in semantics.ord.adj]
AdjunctionsOrdDual.Xr [in semantics.ord.adj]
AdjunctionsOrdDual.Y [in semantics.ord.adj]
AdjunctionsOrdDual.Yr [in semantics.ord.adj]
AdjunctionsOrd.X [in semantics.ord.adj]
AdjunctionsOrd.Y [in semantics.ord.adj]
AssociatedClosure.ic [in semantics.tower.associated_closure]
B
BasisLaws.cov [in semantics.ord.sheaf]BasisLaws.X [in semantics.ord.sheaf]
C
CanonicalBasis.X [in semantics.ord.sheaf]CanonicalCoverage.X [in semantics.ord.sheaf]
Characterization.A [in semantics.tower.associated_closure]
Characterization.closure_operatorT [in semantics.tower.associated_closure]
Characterization.inf_closedT [in semantics.tower.associated_closure]
ClassicalTower.f [in semantics.tower.linear_tower]
ClassicalTower.f_mono [in semantics.tower.linear_tower]
ClassicalTower.X [in semantics.tower.linear_tower]
ClassicalTower.xm [in semantics.tower.linear_tower]
CLatDef.T [in semantics.ord.clat]
CLatLaws.T [in semantics.ord.clat]
CLat.ClassDef.cT [in semantics.ord.clat]
CLat.ClassDef.T [in semantics.ord.clat]
CLat.ClassDef.xT [in semantics.ord.clat]
CmdInduction.P [in semantics.wp.gc]
CmdInduction.p_do [in semantics.wp.gc]
CmdInduction.p_case [in semantics.wp.gc]
CmdInduction.p_seq [in semantics.wp.gc]
CmdInduction.p_assn [in semantics.wp.gc]
CmdInduction.p_skip [in semantics.wp.gc]
CoFinal.e [in semantics.ars]
CoFinal.rho [in semantics.ars]
CoFinal.T [in semantics.ars]
CoFinal.tri [in semantics.ars]
Commutation.T [in semantics.ars]
ComputationN.classical [in semantics.ars]
ComputationN.e [in semantics.ars]
ComputationN.norm [in semantics.ars]
ComputationN.rho [in semantics.ars]
ComputationN.sound [in semantics.ars]
ComputationN.T [in semantics.ars]
CongruenceProofs.congruence_properties [in semantics.ccs.bisim]
CongruenceProofs.R [in semantics.ccs.bisim]
ContFrame.is_embedding [in semantics.ord.cont]
ContinuousSup.dF [in semantics.wp.prelim]
ContinuousSup.F [in semantics.wp.prelim]
ContinuousSup.I [in semantics.wp.prelim]
ContinuousSup.J [in semantics.wp.prelim]
ContinuousSup.j0 [in semantics.wp.prelim]
ContinuousSup.X [in semantics.wp.prelim]
D
Definitions.e [in semantics.ars]Definitions.T [in semantics.ars]
E
EquivalencePaths.A [in semantics.base.fext]EquivalencePaths.B [in semantics.base.fext]
Equivalence.A [in semantics.base.overture]
Equivalence.B [in semantics.base.overture]
EquivProp.A [in semantics.base.overture]
EquivProp.B [in semantics.base.overture]
Evaluation.D [in semantics.f.types]
Evaluation.M [in semantics.f.types]
Evaluation.V [in semantics.f.types]
F
FpCLat.f [in semantics.tower.tarski]FpCLat.X [in semantics.tower.tarski]
FrameLaws.T [in semantics.ord.frame]
Frame.ClassDef.cT [in semantics.ord.frame]
Frame.ClassDef.T [in semantics.ord.frame]
Frame.ClassDef.xT [in semantics.ord.frame]
G
GCInduction.P [in semantics.wp.gc]GCInduction.p_do [in semantics.wp.gc]
GCInduction.p_case [in semantics.wp.gc]
GCInduction.p_seq [in semantics.wp.gc]
GCInduction.p_assn [in semantics.wp.gc]
GCInduction.p_skip [in semantics.wp.gc]
GCInduction.Q [in semantics.wp.gc]
GCInduction.q_cons [in semantics.wp.gc]
GCInduction.q_nil [in semantics.wp.gc]
GfpCompanion.f [in semantics.tower.gfp_companion]
GfpCompanion.f_mono [in semantics.tower.gfp_companion]
GfpCompanion.X [in semantics.tower.gfp_companion]
GlbOrder.f [in semantics.ord.ordtype]
GlbOrder.T [in semantics.ord.ordtype]
GlbOrder.X [in semantics.ord.ordtype]
GlbOrder.Y [in semantics.ord.ordtype]
GlbPreorder.f [in semantics.ord.protype]
GlbPreorder.T [in semantics.ord.protype]
GlbPreorder.X [in semantics.ord.protype]
GlbPreorder.Y [in semantics.ord.protype]
I
InducedOrder.f [in semantics.ord.ordtype]InducedOrder.f_inj [in semantics.ord.ordtype]
InducedOrder.T [in semantics.ord.ordtype]
InducedOrder.X [in semantics.ord.ordtype]
InducedPreorder.f [in semantics.ord.protype]
InducedPreorder.T [in semantics.ord.protype]
InducedPreorder.X [in semantics.ord.protype]
InfClosedCoinduction.f [in semantics.tower.direct_induction]
InfClosedCoinduction.fP [in semantics.tower.direct_induction]
InfClosedCoinduction.H [in semantics.tower.direct_induction]
InfClosedCoinduction.P [in semantics.tower.direct_induction]
InfClosedCoinduction.X [in semantics.tower.direct_induction]
InjectiveSurjective.A [in semantics.base.inhab]
InjectiveSurjective.B [in semantics.base.inhab]
InjectiveSurjective.f [in semantics.base.inhab]
InjectiveSurjective.f_surj [in semantics.base.inhab]
InjectiveSurjective.f_inj [in semantics.base.inhab]
Interval.i0 [in semantics.base.fext]
Interval.i1 [in semantics.base.fext]
IProdCLat.F [in semantics.ord.prod]
IProdCLat.T [in semantics.ord.prod]
IProdFrame.F [in semantics.ord.prod]
IProdFrame.T [in semantics.ord.prod]
IProdLLat.F [in semantics.tower.llat]
IProdLLat.T [in semantics.tower.llat]
IProdOrdType.F [in semantics.ord.prod]
IProdOrdType.T [in semantics.ord.prod]
IProdProType.F [in semantics.ord.prod]
IProdProType.T [in semantics.ord.prod]
J
JLatLaws.T [in semantics.ord.clat]K
KernelOperationsOrder.Xr [in semantics.ord.adj]KernelOperators.Xr [in semantics.ord.adj]
Kleene.f [in semantics.wp.prelim]
Kleene.f_cont [in semantics.wp.prelim]
Kleene.f_mono [in semantics.wp.prelim]
Kleene.X [in semantics.wp.prelim]
L
LatLaws.T [in semantics.ord.clat]LinearTower.f [in semantics.tower.linear_tower]
LinearTower.f_mono [in semantics.tower.linear_tower]
LinearTower.X [in semantics.tower.linear_tower]
LLatLemmas.T [in semantics.tower.llat]
LLat.ClassDef.cT [in semantics.tower.llat]
LLat.ClassDef.T [in semantics.tower.llat]
LLat.ClassDef.xT [in semantics.tower.llat]
LubOrder.f [in semantics.ord.ordtype]
LubOrder.T [in semantics.ord.ordtype]
LubOrder.X [in semantics.ord.ordtype]
LubPreorder.f [in semantics.ord.protype]
LubPreorder.T [in semantics.ord.protype]
LubPreorder.X [in semantics.ord.protype]
M
MFunCLat.X [in semantics.ord.mfun]MFunCLat.Y [in semantics.ord.mfun]
MFunFrame.X [in semantics.ord.mfun]
MFunFrame.Y [in semantics.ord.mfun]
MFun.X [in semantics.ord.mfun]
MFun.Y [in semantics.ord.mfun]
MLatLaws.T [in semantics.ord.clat]
MonoCLat.f [in semantics.ord.mono]
MonoCLat.X [in semantics.ord.mono]
MonoCLat.Y [in semantics.ord.mono]
O
Ord.ClassDef.cT [in semantics.ord.ordtype]Ord.ClassDef.T [in semantics.ord.ordtype]
Ord.ClassDef.xT [in semantics.ord.ordtype]
P
PairCLat.A [in semantics.ord.prod]PairCLat.B [in semantics.ord.prod]
PairFrame.A [in semantics.ord.prod]
PairFrame.B [in semantics.ord.prod]
PairOrdType.A [in semantics.ord.prod]
PairOrdType.B [in semantics.ord.prod]
PairProType.A [in semantics.ord.prod]
PairProType.B [in semantics.ord.prod]
ParameterizedTower.A [in semantics.tower.parameterized]
ParameterizedTower.f [in semantics.tower.parameterized]
ParameterizedTower.f_mono [in semantics.tower.parameterized]
Pataraia.WithFunction.A [in semantics.tower.direct_induction]
Pataraia.WithFunction.f [in semantics.tower.direct_induction]
Pataraia.WithFunction.f_mono [in semantics.tower.direct_induction]
PreorderLemmas.T [in semantics.ord.protype]
PresheafLaws.X [in semantics.ord.presheaf]
PresheafType.X [in semantics.ord.presheaf]
ProdCLat.T [in semantics.ord.prod]
ProdCLat.X [in semantics.ord.prod]
PropInitial.f [in semantics.ord.prop]
PropInitial.X [in semantics.ord.prop]
Pro.ClassDef.cT [in semantics.ord.protype]
Pro.ClassDef.T [in semantics.ord.protype]
PurePropositions.T [in semantics.ord.prop]
Q
QuotientMappingProperty.A [in semantics.base.quotient]QuotientMappingProperty.B [in semantics.base.quotient]
QuotientMappingProperty.R [in semantics.base.quotient]
QuotientTypes.A [in semantics.base.quotient]
QuotientTypes.Induction.f [in semantics.base.quotient]
QuotientTypes.Induction.fP [in semantics.base.quotient]
QuotientTypes.Induction.P [in semantics.base.quotient]
QuotientTypes.R [in semantics.base.quotient]
R
ReverseCLat.X [in semantics.ord.clat]ReverseOrder.T [in semantics.ord.ordtype]
ReversePreorder.T [in semantics.ord.protype]
RightAdjoints.Xr [in semantics.ord.adj]
RightAdjoints.Yr [in semantics.ord.adj]
Rules.T [in semantics.ord.clat]
S
SheafCLat.cov [in semantics.ord.sheaf]SheafCLat.X [in semantics.ord.sheaf]
SheafFrame.cov [in semantics.ord.sheaf]
SheafFrame.X [in semantics.ord.sheaf]
Similarity.A [in semantics.tower.ex_similarity]
Similarity.B [in semantics.tower.ex_similarity]
Similarity.Σ [in semantics.tower.ex_similarity]
Streams.A [in semantics.tower.ex_streams]
SubcanonicalCoverageOrd.b [in semantics.ord.sheaf]
SubcanonicalCoverageOrd.X [in semantics.ord.sheaf]
SubcanonicalCoverage.b [in semantics.ord.sheaf]
SubcanonicalCoverage.X [in semantics.ord.sheaf]
T
TarskiGfp.f [in semantics.tower.tarski]TarskiGfp.fr [in semantics.tower.tarski]
TarskiGfp.X [in semantics.tower.tarski]
TarskiLfp.f [in semantics.tower.tarski]
TarskiLfp.X [in semantics.tower.tarski]
Termination.cr [in semantics.ars]
Termination.e [in semantics.ars]
Termination.T [in semantics.ars]
TowerCompanion.f [in semantics.tower.cocontinuous_tower]
TowerCompanion.f_cocontinuous [in semantics.tower.cocontinuous_tower]
TowerCompanion.f_mono [in semantics.tower.cocontinuous_tower]
TowerCompanion.X [in semantics.tower.cocontinuous_tower]
Tower.DoubleInd.limit [in semantics.tower.tower]
Tower.DoubleInd.R [in semantics.tower.tower]
Tower.DoubleInd.step [in semantics.tower.tower]
Tower.f [in semantics.tower.tower]
Tower.f_mono [in semantics.tower.tower]
Tower.UptoLemmaCharacterization.tt [in semantics.tower.tower]
Tower.UptoLemmaCharacterization.upto [in semantics.tower.tower]
Tower.UptoLemma.g [in semantics.tower.tower]
Tower.UptoLemma.g_mono [in semantics.tower.tower]
Tower.X [in semantics.tower.tower]
TruncationMappingProperty.A [in semantics.base.fext]
TruncationMappingProperty.B [in semantics.base.fext]
Y
YonedaClat.X [in semantics.ord.presheaf]YonedaOrd.X [in semantics.ord.presheaf]
Yoneda.X [in semantics.ord.presheaf]
Library Index
A
abstractadj
ars
associated_closure
B
basebisim
C
churchrosserclat
cocontinuous_tower
compiler
cont
contextmorphism
D
direct_inductionE
ex_streamsex_similarity
F
fcbvreductionfcbvsyntax
fext
fintype
frame
fsemantics
fsyntax
G
gcgcsemantics
gfp_companion
I
icicsemantics
inhab
L
linear_towerllat
M
metamfun
mono
O
ordordtype
overture
P
parameterizedpext
prelim
presheaf
prod
prop
properties
protype
Q
quotientR
realsreduction
reduction
S
semanticssheaf
sorts
states
strongnorm
subjectreduction
subtyping
syntax
syntax
syntax
T
tarskitower
types
typing
W
weaknormLemma Index
A
accn_inv [in semantics.ars]accumulate [in semantics.tower.parameterized]
adjA [in semantics.ord.adj]
adjAc [in semantics.ord.adj]
adjB [in semantics.ord.adj]
adjE [in semantics.ord.adj]
adjEc [in semantics.ord.adj]
adjH [in semantics.ord.adj]
adjJ [in semantics.ord.adj]
adjM [in semantics.ord.adj]
adjP [in semantics.ord.adj]
adjT [in semantics.ord.adj]
adj_tripleR [in semantics.ord.adj]
adj_uniqL [in semantics.ord.adj]
adj_tripleL [in semantics.ord.adj]
adj_uniqR [in semantics.ord.adj]
adj_glb [in semantics.ord.adj]
adj_counit [in semantics.ord.adj]
adj_lub [in semantics.ord.adj]
adj_unit [in semantics.ord.adj]
allc_sigma [in semantics.tower.cocontinuous_tower]
allE [in semantics.ord.clat]
allEc [in semantics.ord.clat]
allI [in semantics.ord.clat]
allIc [in semantics.ord.clat]
all_def [in semantics.ord.clat]
all_mono [in semantics.ord.clat]
all_axiom [in semantics.ord.clat]
all2P [in semantics.wp.gc]
B
basisE [in semantics.ord.sheaf]basisP [in semantics.ord.sheaf]
below_companion_sound [in semantics.tower.parameterized]
below_companion_to_upto [in semantics.tower.tower]
bisim_left [in semantics.ccs.bisim]
bisim_bisim [in semantics.ccs.bisim]
bisim_unfold [in semantics.ccs.bisim]
bisim_fold [in semantics.ccs.bisim]
bisim_coind [in semantics.ccs.bisim]
bisim_eq [in semantics.tower.ex_streams]
bisim_def [in semantics.tower.ex_streams]
botE [in semantics.ord.clat]
bot_def [in semantics.ord.clat]
bot_eq [in semantics.ord.clat]
C
canonicalE [in semantics.ord.sheaf]canonicalP [in semantics.ord.sheaf]
canonical_sup [in semantics.ord.sheaf]
chain_dec [in semantics.tower.cocontinuous_tower]
chuP [in semantics.tower.llat]
church_rosser [in semantics.ccomega.churchrosser]
chu_lt_inf [in semantics.tower.llat]
chu_lt_right [in semantics.tower.llat]
chu_lt_left [in semantics.tower.llat]
chu_infP [in semantics.tower.llat]
chu_le_eq [in semantics.tower.llat]
chu_eq [in semantics.tower.llat]
chu_le_trans [in semantics.tower.llat]
chu_le_refl [in semantics.tower.llat]
classical_tower_max [in semantics.tower.linear_tower]
classical_tower_linear [in semantics.tower.linear_tower]
classical_tower_glue [in semantics.tower.linear_tower]
classical_lt_inf [in semantics.tower.linear_tower]
classical_lt_right [in semantics.tower.linear_tower]
classical_lt_left [in semantics.tower.linear_tower]
classic_mono_to_lmono [in semantics.tower.linear_tower]
closureA [in semantics.ord.adj]
closureAc [in semantics.ord.adj]
closureE [in semantics.ord.adj]
closureEc [in semantics.ord.adj]
closureJ [in semantics.ord.adj]
closureM [in semantics.ord.adj]
closureP [in semantics.ord.adj]
closureT [in semantics.ord.adj]
closure_inf_closed [in semantics.tower.associated_closure]
closure_to_inf_closed_retr [in semantics.tower.associated_closure]
closure_of_image [in semantics.tower.associated_closure]
closure_of_stable [in semantics.tower.associated_closure]
closure_glb [in semantics.ord.adj]
closure_lub [in semantics.ord.adj]
closure_stable [in semantics.ord.adj]
closure_eq [in semantics.ord.adj]
closure_idem [in semantics.ord.adj]
closure_inc [in semantics.ord.adj]
cmd_ind [in semantics.wp.gc]
cmd_eqP [in semantics.wp.gc]
coE [in semantics.tower.gfp_companion]
cofinal_normalizing [in semantics.ars]
companion_coind [in semantics.tower.parameterized]
companion_co [in semantics.tower.gfp_companion]
com_lift [in semantics.ars]
com_strip [in semantics.ars]
confluent_cr [in semantics.ars]
congruence_step [in semantics.ccs.bisim]
contB [in semantics.ord.cont]
contE [in semantics.ord.cont]
contEc [in semantics.ord.cont]
context_ok_ext [in semantics.ccomega.subjectreduction]
contH [in semantics.ord.cont]
continuous_directed_meet_sup [in semantics.wp.prelim]
continuous_directed_meet_sup [in semantics.wp.abstract]
contJ [in semantics.ord.cont]
cont_embH [in semantics.ord.cont]
convES [in semantics.ars]
convESi [in semantics.ars]
conv_closure [in semantics.ars]
conv_hom [in semantics.ars]
conv_img [in semantics.ars]
conv_sym [in semantics.ars]
conv_trans [in semantics.ars]
conv_beta [in semantics.ccomega.reduction]
conv_compat [in semantics.ccomega.reduction]
conv_subst [in semantics.ccomega.reduction]
conv_prod [in semantics.ccomega.reduction]
conv_lam [in semantics.ccomega.reduction]
conv_app [in semantics.ccomega.reduction]
conv_sub [in semantics.ccomega.subtyping]
conv_sub1 [in semantics.ccomega.subtyping]
conv_prod_sort [in semantics.ccomega.churchrosser]
conv_equiv [in semantics.base.quotient]
conv_repr [in semantics.base.quotient]
conv1 [in semantics.ars]
conv1i [in semantics.ars]
coverageP [in semantics.ord.sheaf]
coverage_sheafify_adj [in semantics.ord.sheaf]
coverage_sheafify_inc [in semantics.ord.sheaf]
coverage_trans [in semantics.ord.sheaf]
cover_sup [in semantics.ord.sheaf]
cover_le_trans [in semantics.ord.sheaf]
cover_le_refl [in semantics.ord.sheaf]
co_monotone [in semantics.tower.gfp_companion]
co_greatest_compatible [in semantics.tower.gfp_companion]
co_compatible [in semantics.tower.gfp_companion]
co_upto [in semantics.tower.gfp_companion]
cr_method [in semantics.ars]
cr_conv_normal [in semantics.ars]
cr_star_normal [in semantics.ars]
C_up [in semantics.f.strongnorm]
C_rename [in semantics.f.strongnorm]
C_scons [in semantics.f.strongnorm]
C_upto [in semantics.ccs.properties]
C_inc [in semantics.tower.direct_induction]
C_lfp [in semantics.tower.direct_induction]
D
decreasing_is_below_companion [in semantics.tower.tower]deterministic_to_continuous [in semantics.wp.abstract]
deterministic_sup [in semantics.wp.abstract]
deterministic_sup_closed [in semantics.wp.icsemantics]
diamond_confluent [in semantics.ars]
direct_induction [in semantics.tower.direct_induction]
direct_coinduction [in semantics.tower.direct_induction]
E
embedE [in semantics.ord.sheaf]embedI [in semantics.ord.sheaf]
embedM [in semantics.ord.sheaf]
embedT [in semantics.ord.sheaf]
embed_unembed [in semantics.ord.sheaf]
embed_injective [in semantics.ord.sheaf]
embed_embedding [in semantics.ord.sheaf]
embed_cov [in semantics.ord.sheaf]
embed_def [in semantics.ord.sheaf]
equiv_sect [in semantics.base.overture]
equiv_retr [in semantics.base.overture]
equiv_eq [in semantics.base.fext]
eq_star [in semantics.ars]
evalnP [in semantics.ars]
evaln_sound [in semantics.ars]
eval_lift [in semantics.f.types]
eval_beta [in semantics.f.types]
eval_inst [in semantics.f.types]
eval_weaken [in semantics.f.types]
eval_ren [in semantics.f.types]
eweakening [in semantics.ccomega.contextmorphism]
exE [in semantics.ord.clat]
exEc [in semantics.ord.clat]
exI [in semantics.ord.clat]
exIc [in semantics.ord.clat]
exists_repr [in semantics.base.quotient]
ex_def [in semantics.ord.clat]
ex_mono [in semantics.ord.clat]
ex_axiom [in semantics.ord.clat]
E_beta [in semantics.f.weaknorm]
E_tlam [in semantics.f.strongnorm]
E_tapp [in semantics.f.strongnorm]
E_lam [in semantics.f.strongnorm]
E_app [in semantics.f.strongnorm]
E_beta [in semantics.f.strongnorm]
E_weaken [in semantics.f.strongnorm]
E2_ind [in semantics.f.strongnorm]
F
flip_symmetric [in semantics.ccs.bisim]fp_botE [in semantics.tower.tarski]
fp_topE [in semantics.tower.tarski]
fp_infP [in semantics.tower.tarski]
fp_leE [in semantics.tower.tarski]
fp_eq [in semantics.tower.tarski]
fundamental [in semantics.f.weaknorm]
fundamental [in semantics.f.strongnorm]
f_omega_cocont_strong [in semantics.tower.cocontinuous_tower]
G
gfpE [in semantics.tower.tarski]gfp_const [in semantics.wp.compiler]
gfp_def [in semantics.tower.tarski]
gfp_belowE [in semantics.tower.tarski]
gfp_below_unfold [in semantics.tower.tarski]
gfp_below_le [in semantics.tower.tarski]
gfp_below_coind [in semantics.tower.tarski]
glbE [in semantics.ord.protype]
glbP [in semantics.ord.protype]
glb_uniq [in semantics.ord.ordtype]
glb_lb [in semantics.ord.protype]
gtestP [in semantics.wp.compiler]
gtest_contra [in semantics.wp.compiler]
gtest_cons [in semantics.wp.compiler]
H
hoare_do [in semantics.wp.gcsemantics]hoare_case [in semantics.wp.gcsemantics]
hoare_seq [in semantics.wp.gcsemantics]
hoare_act [in semantics.wp.gcsemantics]
hoare_skip [in semantics.wp.gcsemantics]
I
id_rcomp [in semantics.ccs.syntax]id_inst [in semantics.ccs.syntax]
impBx [in semantics.ord.frame]
impEl [in semantics.ord.frame]
impEr [in semantics.ord.frame]
impEx [in semantics.ord.frame]
impI [in semantics.ord.frame]
impJx [in semantics.ord.frame]
impMx [in semantics.ord.frame]
impP [in semantics.ord.frame]
impTx [in semantics.ord.frame]
impxA [in semantics.ord.frame]
impxJ [in semantics.ord.frame]
impxM [in semantics.ord.frame]
impxT [in semantics.ord.frame]
impxx [in semantics.ord.frame]
imp_def [in semantics.ord.frame]
imp_cut [in semantics.ord.frame]
induced_le_eq [in semantics.ord.ordtype]
induced_le_trans [in semantics.ord.protype]
induced_le_refl [in semantics.ord.protype]
inf_closed_to_closure_retr [in semantics.tower.associated_closure]
inf_closed_wpi_distributive [in semantics.wp.icsemantics]
inf_closed_coind [in semantics.tower.direct_induction]
inf_closed_wp_distributive [in semantics.wp.gcsemantics]
inhab_prop [in semantics.base.inhab]
inhab_map_retr [in semantics.base.fext]
inhab_map_sect [in semantics.base.fext]
injP [in semantics.wp.gc]
inj_prod [in semantics.ccomega.churchrosser]
inj_sort [in semantics.ccomega.churchrosser]
inst_comp [in semantics.wp.ic]
inst_rinst_comp [in semantics.wp.ic]
inst_ids [in semantics.wp.ic]
inst_id [in semantics.ccs.syntax]
inst_comp [in semantics.f.fsyntax]
inst_ren_comp [in semantics.f.fsyntax]
inst_ids [in semantics.f.fsyntax]
inst_comp [in semantics.debruijn.syntax]
inst_ren_comp [in semantics.debruijn.syntax]
inst_ids [in semantics.debruijn.syntax]
inst_shift [in semantics.debruijn.syntax]
inst_bound [in semantics.debruijn.syntax]
inst_lam [in semantics.debruijn.syntax]
inst_app [in semantics.debruijn.syntax]
inst_comp [in semantics.ccomega.syntax]
inst_ren_comp [in semantics.ccomega.syntax]
inst_ids [in semantics.ccomega.syntax]
interval_lt_inf [in semantics.tower.reals]
interval_lt_right [in semantics.tower.reals]
interval_lt_left [in semantics.tower.reals]
interval_inf_axiom [in semantics.tower.reals]
interval_le_eq [in semantics.tower.reals]
interval_le_trans [in semantics.tower.reals]
interval_le_refl [in semantics.tower.reals]
interval_eq [in semantics.tower.reals]
inverse_cand_retraction [in semantics.base.inhab]
inverse_cand_section [in semantics.base.inhab]
in_classE [in semantics.base.quotient]
iprod_leE [in semantics.ord.prod]
iprod_impE [in semantics.ord.prod]
iprod_frameP [in semantics.ord.prod]
iprod_allE [in semantics.ord.prod]
iprod_exE [in semantics.ord.prod]
iprod_meetE [in semantics.ord.prod]
iprod_joinE [in semantics.ord.prod]
iprod_botE [in semantics.ord.prod]
iprod_topE [in semantics.ord.prod]
iprod_infP [in semantics.ord.prod]
iprod_le_eq [in semantics.ord.prod]
iprod_le_trans [in semantics.ord.prod]
iprod_le_refl [in semantics.ord.prod]
iprod_lt_inf [in semantics.tower.llat]
iprod_lt_right [in semantics.tower.llat]
iprod_lt_left [in semantics.tower.llat]
is_type_weakening [in semantics.ccomega.subjectreduction]
is_finite_lam [in semantics.ccomega.subjectreduction]
is_finite_prod [in semantics.ccomega.subjectreduction]
is_finite_var [in semantics.ccomega.subjectreduction]
is_equiv_prop [in semantics.base.fext]
is_sheaf_exponential_ideal [in semantics.ord.sheaf]
is_sheaf_inf_closed [in semantics.ord.sheaf]
iter_mono [in semantics.wp.prelim]
I_path [in semantics.base.fext]
J
joinA [in semantics.ord.clat]joinAC [in semantics.ord.clat]
joinACA [in semantics.ord.clat]
joinBx [in semantics.ord.clat]
joinC [in semantics.ord.clat]
joinCA [in semantics.ord.clat]
joinE [in semantics.ord.clat]
joinIl [in semantics.ord.clat]
joinIr [in semantics.ord.clat]
joinKx [in semantics.ord.clat]
joinTx [in semantics.ord.clat]
joinxB [in semantics.ord.clat]
joinxK [in semantics.ord.clat]
joinxT [in semantics.ord.clat]
joinxx [in semantics.ord.clat]
join_conv [in semantics.ars]
join_def [in semantics.ord.clat]
join_mono [in semantics.ord.clat]
join_axiom [in semantics.ord.clat]
K
kernelP [in semantics.ord.adj]kernel_lub [in semantics.ord.adj]
kernel_glb [in semantics.ord.adj]
kernel_stable [in semantics.ord.adj]
kernel_eq [in semantics.ord.adj]
kernel_idem [in semantics.ord.adj]
kernel_dec [in semantics.ord.adj]
kleene_fp [in semantics.wp.prelim]
kleene_t_is_t [in semantics.tower.cocontinuous_tower]
kleene_compat [in semantics.tower.cocontinuous_tower]
K_weaken [in semantics.f.strongnorm]
K_all [in semantics.f.strongnorm]
K_arr [in semantics.f.strongnorm]
K_var [in semantics.f.strongnorm]
L
lbP [in semantics.ord.protype]le_eq [in semantics.ord.ordtype]
le_trans [in semantics.ord.protype]
le_refl [in semantics.ord.protype]
le_meetP [in semantics.ord.clat]
le_joinP [in semantics.ord.clat]
lfpE [in semantics.tower.tarski]
lfp_const [in semantics.wp.compiler]
lfp_def [in semantics.tower.tarski]
lfp_aboveE [in semantics.tower.tarski]
lfp_above_fold [in semantics.tower.tarski]
lfp_above_ge [in semantics.tower.tarski]
lfp_above_ind [in semantics.tower.tarski]
loop_countable_branching_not_similar [in semantics.tower.ex_similarity]
loop_countable_branching_nsim [in semantics.tower.ex_similarity]
lt_inf [in semantics.tower.llat]
lt_right [in semantics.tower.llat]
lt_left [in semantics.tower.llat]
lubE [in semantics.ord.protype]
lubP [in semantics.ord.protype]
lub_uniq [in semantics.ord.ordtype]
lub_ub [in semantics.ord.protype]
M
map_subst [in semantics.ccs.syntax]meetA [in semantics.ord.clat]
meetAC [in semantics.ord.clat]
meetACA [in semantics.ord.clat]
meetBx [in semantics.ord.clat]
meetC [in semantics.ord.clat]
meetCA [in semantics.ord.clat]
meetEl [in semantics.ord.clat]
meetEr [in semantics.ord.clat]
meetEx [in semantics.ord.frame]
meetHl [in semantics.ord.frame]
meetHr [in semantics.ord.frame]
meetI [in semantics.ord.clat]
meetJx [in semantics.ord.frame]
meetKx [in semantics.ord.clat]
meetTx [in semantics.ord.clat]
meetxB [in semantics.ord.clat]
meetxE [in semantics.ord.frame]
meetxJ [in semantics.ord.frame]
meetxK [in semantics.ord.clat]
meetxT [in semantics.ord.clat]
meetxx [in semantics.ord.clat]
meet_def [in semantics.ord.clat]
meet_mono [in semantics.ord.clat]
meet_axiom [in semantics.ord.clat]
mfun_impE [in semantics.ord.mfun]
mfun_frameP [in semantics.ord.mfun]
mfun_allE [in semantics.ord.mfun]
mfun_exE [in semantics.ord.mfun]
mfun_meetE [in semantics.ord.mfun]
mfun_joinE [in semantics.ord.mfun]
mfun_botE [in semantics.ord.mfun]
mfun_topE [in semantics.ord.mfun]
mfun_infP [in semantics.ord.mfun]
mfun_leE [in semantics.ord.mfun]
mfun_eq [in semantics.ord.mfun]
mk_glb [in semantics.ord.protype]
mk_lub [in semantics.ord.protype]
mono [in semantics.ord.mono]
monoA [in semantics.ord.mono]
monoAc [in semantics.ord.mono]
monoE [in semantics.ord.mono]
monoEc [in semantics.ord.mono]
monoJ [in semantics.ord.mono]
monoM [in semantics.ord.mono]
monotone_unembed [in semantics.ord.sheaf]
N
nat_le_E [in semantics.ccomega.sorts]nat_le_eq [in semantics.ccomega.sorts]
nat_le_trans [in semantics.ccomega.sorts]
nat_le_refl [in semantics.ccomega.sorts]
nf_accn [in semantics.ars]
normal_star [in semantics.ars]
normal_step_sort [in semantics.ccomega.churchrosser]
O
obisim_unfold_mu [in semantics.ccs.bisim]obisim_coind [in semantics.ccs.bisim]
P
pairb_fun [in semantics.base.fext]pair_impE [in semantics.ord.prod]
pair_frameP [in semantics.ord.prod]
pair_allE [in semantics.ord.prod]
pair_exE [in semantics.ord.prod]
pair_meetE [in semantics.ord.prod]
pair_joinE [in semantics.ord.prod]
pair_botE [in semantics.ord.prod]
pair_topE [in semantics.ord.prod]
pair_infP [in semantics.ord.prod]
pair_le_eq [in semantics.ord.prod]
pair_le_trans [in semantics.ord.prod]
pair_le_refl [in semantics.ord.prod]
parameterized_tower_ind_s [in semantics.tower.parameterized]
parameterized_tower_ind [in semantics.tower.parameterized]
Pataraia.infl_nullP [in semantics.tower.direct_induction]
Pataraia.infl_null_T [in semantics.tower.direct_induction]
Pataraia.infl_codirected [in semantics.tower.direct_induction]
Pataraia.infl_comp [in semantics.tower.direct_induction]
Pataraia.infl_id [in semantics.tower.direct_induction]
Pataraia.infl_f [in semantics.tower.direct_induction]
Pataraia.T_dec [in semantics.tower.direct_induction]
Pataraia.T_top [in semantics.tower.direct_induction]
Pataraia.ν_gfp [in semantics.tower.direct_induction]
Pataraia.ν_coind [in semantics.tower.direct_induction]
Pataraia.ν_min [in semantics.tower.direct_induction]
Pataraia.ν_inc [in semantics.tower.direct_induction]
Pataraia.ν_tower [in semantics.tower.direct_induction]
pext [in semantics.base.pext]
pi [in semantics.base.pext]
presheafP [in semantics.ord.presheaf]
presheaf_representables [in semantics.ord.presheaf]
presheaf_impE [in semantics.ord.presheaf]
presheaf_allEc [in semantics.ord.presheaf]
presheaf_exEc [in semantics.ord.presheaf]
presheaf_allE [in semantics.ord.presheaf]
presheaf_exE [in semantics.ord.presheaf]
presheaf_meetE [in semantics.ord.presheaf]
presheaf_joinE [in semantics.ord.presheaf]
presheaf_topE [in semantics.ord.presheaf]
presheaf_botE [in semantics.ord.presheaf]
presheaf_leE [in semantics.ord.presheaf]
presheaf_of_imp [in semantics.ord.sheaf]
prod_impE [in semantics.ord.prod]
prod_allE [in semantics.ord.prod]
prod_exE [in semantics.ord.prod]
prod_meetE [in semantics.ord.prod]
prod_joinE [in semantics.ord.prod]
prod_botE [in semantics.ord.prod]
prod_topE [in semantics.ord.prod]
prod_leE [in semantics.ord.prod]
prod_is_prop [in semantics.base.fext]
prod_exEc [in semantics.tower.ex_similarity]
propagation [in semantics.ccomega.subjectreduction]
prop_initial [in semantics.ord.prop]
prop_impE [in semantics.ord.prop]
prop_frameP [in semantics.ord.prop]
prop_allEc [in semantics.ord.prop]
prop_exEc [in semantics.ord.prop]
prop_allE [in semantics.ord.prop]
prop_exE [in semantics.ord.prop]
prop_meetE [in semantics.ord.prop]
prop_joinE [in semantics.ord.prop]
prop_botE [in semantics.ord.prop]
prop_topE [in semantics.ord.prop]
prop_infP [in semantics.ord.prop]
prop_le_eq [in semantics.ord.prop]
prop_leE [in semantics.ord.prop]
prop_le_trans [in semantics.ord.prop]
prop_le_refl [in semantics.ord.prop]
psstep_up [in semantics.ccomega.churchrosser]
pstep_compat_beta [in semantics.ccomega.churchrosser]
pstep_compat [in semantics.ccomega.churchrosser]
pstep_subst [in semantics.ccomega.churchrosser]
pstep_red [in semantics.ccomega.churchrosser]
pstep_refl [in semantics.ccomega.churchrosser]
pureA [in semantics.ord.prop]
pureB [in semantics.ord.prop]
pureE [in semantics.ord.prop]
pureH [in semantics.ord.prop]
pureI [in semantics.ord.prop]
pureJ [in semantics.ord.prop]
pureM [in semantics.ord.prop]
pureS [in semantics.ord.prop]
pureT [in semantics.ord.prop]
pure_sup [in semantics.ord.prop]
pure_inf [in semantics.ord.prop]
pure_eq [in semantics.ord.prop]
Q
quot_map_retr [in semantics.base.quotient]quot_map_sect [in semantics.base.quotient]
quot_rectE [in semantics.base.quotient]
R
rbindA [in semantics.ccs.syntax]rbind_rmap_comp [in semantics.ccs.syntax]
rbisim_equivalence [in semantics.tower.ex_streams]
rbisim_refl [in semantics.tower.ex_streams]
rcompA [in semantics.ccs.syntax]
rcomp_id [in semantics.ccs.syntax]
red_compat [in semantics.ccomega.reduction]
red_subst [in semantics.ccomega.reduction]
red_prod [in semantics.ccomega.reduction]
red_lam [in semantics.ccomega.reduction]
red_app [in semantics.ccomega.reduction]
red_prod_inv [in semantics.ccomega.churchrosser]
ren_comp [in semantics.f.fsyntax]
ren_inst_comp [in semantics.f.fsyntax]
ren_inst [in semantics.f.fsyntax]
ren_id [in semantics.f.fsyntax]
ren_comp [in semantics.debruijn.syntax]
ren_inst_comp [in semantics.debruijn.syntax]
ren_id [in semantics.debruijn.syntax]
ren_inst [in semantics.debruijn.syntax]
ren_comp [in semantics.ccomega.syntax]
ren_inst_comp [in semantics.ccomega.syntax]
ren_inst [in semantics.ccomega.syntax]
ren_id [in semantics.ccomega.syntax]
reprP [in semantics.base.quotient]
repr_equiv [in semantics.base.quotient]
repr_conv [in semantics.base.quotient]
repr_surjective [in semantics.base.quotient]
restrictE [in semantics.ord.sheaf]
restrictP [in semantics.ord.sheaf]
restrict_restrict [in semantics.ord.sheaf]
restrict_top [in semantics.ord.sheaf]
restrict_refl [in semantics.ord.sheaf]
reverse_le_eq [in semantics.ord.ordtype]
reverse_le_trans [in semantics.ord.protype]
reverse_le_refl [in semantics.ord.protype]
rev_leE [in semantics.ord.protype]
rev_exEc [in semantics.ord.clat]
rev_exE [in semantics.ord.clat]
rev_allEc [in semantics.ord.clat]
rev_allE [in semantics.ord.clat]
rev_infP [in semantics.ord.clat]
rev_lfp [in semantics.tower.direct_induction]
rho_triangle [in semantics.ccomega.churchrosser]
rinst_compF [in semantics.wp.ic]
rinst_comp [in semantics.wp.ic]
rinst_inst_comp [in semantics.wp.ic]
rinst_id [in semantics.wp.ic]
rinst_inst [in semantics.wp.ic]
rmap_rbind_comp [in semantics.ccs.syntax]
rmap_comp [in semantics.ccs.syntax]
R_rename [in semantics.f.strongnorm]
R_var [in semantics.f.strongnorm]
R_step [in semantics.f.strongnorm]
R_sn [in semantics.f.strongnorm]
S
scomp_assoc [in semantics.debruijn.syntax]scomp_id [in semantics.debruijn.syntax]
scomp_id_l [in semantics.debruijn.syntax]
scons_scomp [in semantics.ccs.syntax]
scons_scomp_eta [in semantics.debruijn.syntax]
scons_inst_eta_id [in semantics.debruijn.syntax]
scons_inst_eta [in semantics.debruijn.syntax]
scons_comp [in semantics.data.fintype]
scons_eta_id [in semantics.data.fintype]
scons_eta [in semantics.data.fintype]
sconv_up [in semantics.ccomega.reduction]
sheafifyB [in semantics.ord.sheaf]
sheafifyE [in semantics.ord.sheaf]
sheafifyEc [in semantics.ord.sheaf]
sheafifyJ [in semantics.ord.sheaf]
sheafifyM [in semantics.ord.sheaf]
sheafifyT [in semantics.ord.sheaf]
sheafify_def [in semantics.ord.sheaf]
sheafify_strong [in semantics.ord.sheaf]
sheafify_imp_ideal [in semantics.ord.sheaf]
sheafify_is_sheaf [in semantics.ord.sheaf]
sheafify_idem [in semantics.ord.sheaf]
sheafify_inc [in semantics.ord.sheaf]
sheafP [in semantics.ord.sheaf]
sheaf_pureE [in semantics.ord.sheaf]
sheaf_exEc [in semantics.ord.sheaf]
sheaf_exE [in semantics.ord.sheaf]
sheaf_joinE [in semantics.ord.sheaf]
sheaf_botE [in semantics.ord.sheaf]
sheaf_coverageP [in semantics.ord.sheaf]
sheaf_impE [in semantics.ord.sheaf]
sheaf_frameP [in semantics.ord.sheaf]
sheaf_impP [in semantics.ord.sheaf]
sheaf_representables [in semantics.ord.sheaf]
sheaf_exIc [in semantics.ord.sheaf]
sheaf_exI [in semantics.ord.sheaf]
sheaf_joinI [in semantics.ord.sheaf]
sheaf_exc_sheafify [in semantics.ord.sheaf]
sheaf_ex_sheafify [in semantics.ord.sheaf]
sheaf_join_sheafify [in semantics.ord.sheaf]
sheaf_bot_sheafify [in semantics.ord.sheaf]
sheaf_meetE [in semantics.ord.sheaf]
sheaf_topE [in semantics.ord.sheaf]
sheaf_allEc [in semantics.ord.sheaf]
sheaf_allE [in semantics.ord.sheaf]
sheaf_infP [in semantics.ord.sheaf]
sheaf_leE [in semantics.ord.sheaf]
sheaf_eq [in semantics.ord.sheaf]
shift_scons [in semantics.ccs.syntax]
shift_up [in semantics.data.fintype]
sieveP [in semantics.ord.sheaf]
sieve_eq [in semantics.ord.sheaf]
sigT_is_hprop [in semantics.base.overture]
sigT_eq [in semantics.base.overture]
sigT_injective [in semantics.base.pext]
sig_is_hprop [in semantics.base.pext]
sig_eq [in semantics.base.pext]
similar_def [in semantics.tower.ex_similarity]
sn_wn [in semantics.ars]
sn_preimage [in semantics.ars]
sort_le_typeE [in semantics.ccomega.sorts]
sort_le_eq [in semantics.ccomega.sorts]
sort_le_trans [in semantics.ccomega.sorts]
sort_le_refl [in semantics.ccomega.sorts]
sred_up [in semantics.ccomega.reduction]
starES [in semantics.ars]
star_interpolation [in semantics.ars]
star_monotone [in semantics.ars]
star_closure [in semantics.ars]
star_hom [in semantics.ars]
star_img [in semantics.ars]
star_conv [in semantics.ars]
star_trans [in semantics.ars]
star1 [in semantics.ars]
step_subst [in semantics.ccomega.reduction]
step_fix_inv [in semantics.ccs.semantics]
step_new_inv [in semantics.ccs.semantics]
step_par_inv [in semantics.ccs.semantics]
step_sum_inv [in semantics.ccs.semantics]
step_act_inv [in semantics.ccs.semantics]
step_pstep [in semantics.ccomega.churchrosser]
step_inst [in semantics.f.fsemantics]
step_weak [in semantics.f.fsemantics]
stream_companionP [in semantics.tower.ex_streams]
strong_normalization [in semantics.f.strongnorm]
subcanonical_embedE [in semantics.ord.sheaf]
subject_reduction [in semantics.ccomega.subjectreduction]
substitutivity [in semantics.debruijn.reduction]
subst_up [in semantics.ccs.syntax]
subst_extend [in semantics.ccs.syntax]
sub_inst [in semantics.ccomega.subtyping]
sub_prod_inv [in semantics.ccomega.subtyping]
sub_trans [in semantics.ccomega.subtyping]
sub_sort [in semantics.ccomega.subtyping]
sub_refl [in semantics.ccomega.subtyping]
sub1_inst [in semantics.ccomega.subtyping]
sub1_trans [in semantics.ccomega.subtyping]
sub1_conv [in semantics.ccomega.subtyping]
sub1_sub [in semantics.ccomega.subtyping]
sup_closed_wpi_distributive [in semantics.wp.icsemantics]
sup_closed_wp_distributive [in semantics.wp.gcsemantics]
sup_canonical [in semantics.ord.sheaf]
T
tag_injective [in semantics.base.overture]terminates_def [in semantics.wp.icsemantics]
tm_inst_comp [in semantics.f.fcbvsyntax]
tm_inst_ren_comp [in semantics.f.fcbvsyntax]
tm_ren_comp [in semantics.f.fcbvsyntax]
tm_ren_inst_comp [in semantics.f.fcbvsyntax]
tm_inst_ids [in semantics.f.fcbvsyntax]
tm_ren_inst [in semantics.f.fcbvsyntax]
tm_ren_id [in semantics.f.fcbvsyntax]
topI [in semantics.ord.clat]
top_def [in semantics.ord.clat]
top_eq [in semantics.ord.clat]
tower_wf [in semantics.tower.linear_tower]
tower_linear [in semantics.tower.linear_tower]
tower_linear_right [in semantics.tower.linear_tower]
tower_linear_left [in semantics.tower.linear_tower]
tower_f_linear [in semantics.tower.linear_tower]
tower_induction [in semantics.tower.tower]
tower_dec [in semantics.tower.tower]
transport_const [in semantics.base.overture]
triangle_cofinal [in semantics.ars]
triangle_monotone [in semantics.ars]
triangle_diamond [in semantics.ars]
tup_ids [in semantics.f.types]
tv_inst_comp [in semantics.f.fcbvsyntax]
tv_inst_ren_comp [in semantics.f.fcbvsyntax]
tv_ren_inst_comp [in semantics.f.fcbvsyntax]
tv_ren_inst [in semantics.f.fcbvsyntax]
tv_ren_id [in semantics.f.fcbvsyntax]
tysubst_upi [in semantics.ccomega.contextmorphism]
tysubst_up [in semantics.ccomega.contextmorphism]
tysubst_cons [in semantics.ccomega.contextmorphism]
tysubst_shift [in semantics.ccomega.contextmorphism]
tysubst_ren_comp [in semantics.ccomega.contextmorphism]
tysubst_comp [in semantics.ccomega.contextmorphism]
tysubst_var [in semantics.ccomega.contextmorphism]
tysubst_ids [in semantics.ccomega.contextmorphism]
ty_prod_wf [in semantics.ccomega.typing]
ty_sort_wf [in semantics.ccomega.typing]
ty_eapp [in semantics.ccomega.typing]
ty_scomp_assoc [in semantics.f.types]
ty_inst_comp [in semantics.f.types]
ty_tup_comp [in semantics.f.types]
ty_inst_ren_comp [in semantics.f.types]
ty_tup_up_comp [in semantics.f.types]
ty_ren_comp [in semantics.f.types]
ty_ren_inst_comp [in semantics.f.types]
ty_scomp_idR [in semantics.f.types]
ty_inst_ids [in semantics.f.types]
ty_ren_id [in semantics.f.types]
ty_ren_inst [in semantics.f.types]
ty_ctx_conv [in semantics.ccomega.contextmorphism]
ty_cut [in semantics.ccomega.contextmorphism]
ty_subst [in semantics.ccomega.contextmorphism]
ty_map [in semantics.ccomega.contextmorphism]
ty_lam_inv [in semantics.ccomega.subjectreduction]
ty_lam_invX [in semantics.ccomega.subjectreduction]
ty_prod_inv [in semantics.ccomega.subjectreduction]
ty_prod_invX [in semantics.ccomega.subjectreduction]
T_kleene [in semantics.tower.cocontinuous_tower]
T_iter [in semantics.tower.cocontinuous_tower]
t_greatest_respectful [in semantics.tower.tower]
t_greatest_compatible [in semantics.tower.tower]
t_compat [in semantics.tower.tower]
t_fdec [in semantics.tower.tower]
t_gfp [in semantics.tower.tower]
t_f [in semantics.tower.tower]
t_img [in semantics.tower.tower]
t_idem [in semantics.tower.tower]
t_inc [in semantics.tower.tower]
T_t [in semantics.tower.tower]
T_ind2 [in semantics.tower.tower]
T_C [in semantics.tower.direct_induction]
T_dec [in semantics.tower.direct_induction]
T_gfp [in semantics.tower.direct_induction]
U
ubP [in semantics.ord.protype]unembed_embed [in semantics.ord.sheaf]
unique_solutions1 [in semantics.ccs.properties]
unique_solutions [in semantics.ccs.properties]
unit_is_hprop [in semantics.base.overture]
upE [in semantics.ccs.syntax]
upi_comp [in semantics.wp.ic]
upi_comp [in semantics.f.fsyntax]
upi_up_comp [in semantics.f.fsyntax]
upi_ids [in semantics.f.fsyntax]
upi_comp [in semantics.debruijn.syntax]
upi_up_comp [in semantics.debruijn.syntax]
upi_ids [in semantics.debruijn.syntax]
upi_def [in semantics.debruijn.syntax]
upi_comp [in semantics.ccomega.syntax]
upi_up_comp [in semantics.ccomega.syntax]
upi_ids [in semantics.ccomega.syntax]
upi_ids [in semantics.f.fcbvsyntax]
upr_up [in semantics.ccs.syntax]
upto_inst [in semantics.ccs.bisim]
upto_fix_o [in semantics.ccs.bisim]
upto_fix_gen [in semantics.ccs.bisim]
upto_inst_beta' [in semantics.ccs.bisim]
upto_inst' [in semantics.ccs.bisim]
upto_new_o [in semantics.ccs.bisim]
upto_par_o [in semantics.ccs.bisim]
upto_act_s_open [in semantics.ccs.bisim]
upto_act_s [in semantics.ccs.bisim]
upto_context [in semantics.tower.ex_streams]
upto_to_tower_induction [in semantics.tower.tower]
upto_lemma [in semantics.tower.tower]
up_comp [in semantics.ccs.syntax]
up_upr [in semantics.ccs.syntax]
up_ren [in semantics.ccs.syntax]
up_id [in semantics.ccs.syntax]
V
vl_inst_comp [in semantics.f.fcbvsyntax]vl_inst_ren_comp [in semantics.f.fcbvsyntax]
vl_ren_comp [in semantics.f.fcbvsyntax]
vl_ren_inst_comp [in semantics.f.fcbvsyntax]
vl_inst_ids [in semantics.f.fcbvsyntax]
vl_ren_inst [in semantics.f.fcbvsyntax]
vl_ren_id [in semantics.f.fcbvsyntax]
vup_comp [in semantics.f.fcbvsyntax]
vup_up_comp [in semantics.f.fcbvsyntax]
V_beta [in semantics.f.weaknorm]
V_weaken [in semantics.f.weaknorm]
V_all [in semantics.f.weaknorm]
V_arr [in semantics.f.weaknorm]
V_to_E [in semantics.f.weaknorm]
V_beta [in semantics.f.strongnorm]
V_weaken [in semantics.f.strongnorm]
W
weaken [in semantics.ord.frame]weakening [in semantics.ccomega.contextmorphism]
weakly_guarded_inst [in semantics.ccs.properties]
weak_normalization [in semantics.f.weaknorm]
wlpi_compile_correct [in semantics.wp.compiler]
wlpi_comp [in semantics.wp.compiler]
wlpi_flatmapF [in semantics.wp.compiler]
wlpi_flatmapT [in semantics.wp.compiler]
wlpi_flatmap [in semantics.wp.compiler]
wlpi_let [in semantics.wp.compiler]
wlpi_eval [in semantics.wp.icsemantics]
wlpi_mstep [in semantics.wp.icsemantics]
wlpi_step [in semantics.wp.icsemantics]
wlpi_is_distributive [in semantics.wp.icsemantics]
wlpi_distributes_over_wpi [in semantics.wp.icsemantics]
wlpi_beta [in semantics.wp.icsemantics]
wlpi_inst [in semantics.wp.icsemantics]
wlpi_weaken [in semantics.wp.icsemantics]
wlpi_ren [in semantics.wp.icsemantics]
wlpi_def [in semantics.wp.icsemantics]
wlpi_def_gfp [in semantics.wp.icsemantics]
wlpi_if [in semantics.wp.icsemantics]
wlpi_jump [in semantics.wp.icsemantics]
wlpi_act [in semantics.wp.icsemantics]
wlps_to_wlp [in semantics.wp.gcsemantics]
wlp_to_wp [in semantics.wp.abstract]
wlp_distributes_over [in semantics.wp.abstract]
wlp_distributes_over_wp [in semantics.wp.abstract]
wlp_distributive [in semantics.wp.abstract]
wlp_mono [in semantics.wp.abstract]
wlp_is_distributive [in semantics.wp.gcsemantics]
wlp_distributes_over_wp [in semantics.wp.gcsemantics]
wlp_wlps_equiv [in semantics.wp.gcsemantics]
wlp_to_wlps [in semantics.wp.gcsemantics]
wlp_do [in semantics.wp.gcsemantics]
wlp_case [in semantics.wp.gcsemantics]
wlp_seq [in semantics.wp.gcsemantics]
wlp_act [in semantics.wp.gcsemantics]
wlp_skip [in semantics.wp.gcsemantics]
wn_accn [in semantics.ars]
wpF_distributive [in semantics.wp.gcsemantics]
wpG_eqn [in semantics.wp.gcsemantics]
wpi_compile_correct [in semantics.wp.compiler]
wpi_comp [in semantics.wp.compiler]
wpi_flatmapF [in semantics.wp.compiler]
wpi_flatmapT [in semantics.wp.compiler]
wpi_flatmap [in semantics.wp.compiler]
wpi_let [in semantics.wp.compiler]
wpi_operational [in semantics.wp.icsemantics]
wpi_terminates [in semantics.wp.icsemantics]
wpi_terminates_subst [in semantics.wp.icsemantics]
wpi_eval [in semantics.wp.icsemantics]
wpi_mstep [in semantics.wp.icsemantics]
wpi_step [in semantics.wp.icsemantics]
wpi_lfp_kleene [in semantics.wp.icsemantics]
wpi_Ω [in semantics.wp.icsemantics]
wpi_deterministic [in semantics.wp.icsemantics]
wpi_is_distributive [in semantics.wp.icsemantics]
wpI_distributive [in semantics.wp.icsemantics]
wpi_beta [in semantics.wp.icsemantics]
wpi_inst [in semantics.wp.icsemantics]
wpi_weaken [in semantics.wp.icsemantics]
wpi_ren [in semantics.wp.icsemantics]
wpI_ren_compat [in semantics.wp.icsemantics]
wpi_def [in semantics.wp.icsemantics]
wpi_def_lfp [in semantics.wp.icsemantics]
wpi_if [in semantics.wp.icsemantics]
wpi_jump [in semantics.wp.icsemantics]
wpi_act [in semantics.wp.icsemantics]
wpn_mono [in semantics.wp.icsemantics]
wps_to_wp [in semantics.wp.gcsemantics]
wp_deterministic [in semantics.wp.abstract]
wp_continuous [in semantics.wp.abstract]
wp_distributive_over [in semantics.wp.abstract]
wp_distributive [in semantics.wp.abstract]
wp_mono [in semantics.wp.abstract]
wp_to_wlp [in semantics.wp.abstract]
wp_continuous [in semantics.wp.gcsemantics]
wp_wpG_continuous [in semantics.wp.gcsemantics]
wp_is_distributive [in semantics.wp.gcsemantics]
wp_wps_equiv [in semantics.wp.gcsemantics]
wp_to_wps [in semantics.wp.gcsemantics]
wp_do [in semantics.wp.gcsemantics]
wp_case [in semantics.wp.gcsemantics]
wp_seq [in semantics.wp.gcsemantics]
wp_act [in semantics.wp.gcsemantics]
wp_skip [in semantics.wp.gcsemantics]
wp_do_eqn [in semantics.wp.gcsemantics]
wp_mono [in semantics.wp.gcsemantics]
X
xi_extS [in semantics.base.fext]xi_extP [in semantics.base.fext]
xi_ext [in semantics.base.fext]
Y
yoneda [in semantics.ord.presheaf]yo_meet [in semantics.ord.presheaf]
yo_top [in semantics.ord.presheaf]
yo_inf [in semantics.ord.presheaf]
yo_injective [in semantics.ord.presheaf]
yo_limit [in semantics.ord.presheaf]
yo_embedding [in semantics.ord.presheaf]
other
ε_cocontinuous [in semantics.tower.ex_streams]Constructor Index
A
accnH [in semantics.ars]accnL [in semantics.ars]
acc_on_i [in semantics.tower.linear_tower]
Act [in semantics.wp.ic]
Act [in semantics.ccs.syntax]
ActRecv [in semantics.ccs.syntax]
ActSend [in semantics.ccs.syntax]
ActTau [in semantics.ccs.syntax]
all [in semantics.f.types]
app [in semantics.f.fsyntax]
app [in semantics.debruijn.syntax]
app [in semantics.ccomega.syntax]
app [in semantics.f.fcbvsyntax]
arr [in semantics.f.types]
Assn [in semantics.wp.gc]
C
Case [in semantics.wp.gc]CLat.Class [in semantics.ord.clat]
CLat.Mixin [in semantics.ord.clat]
CLat.Pack [in semantics.ord.clat]
convR [in semantics.ars]
convSE [in semantics.ars]
convSEi [in semantics.ars]
convxx [in semantics.base.quotient]
conv1R [in semantics.base.quotient]
conv1S [in semantics.base.quotient]
cover_cover [in semantics.ord.sheaf]
cover_max [in semantics.ord.sheaf]
CtxOperator [in semantics.tower.ex_streams]
C_ctx [in semantics.ccs.properties]
C_trans [in semantics.ccs.properties]
C_sym [in semantics.ccs.properties]
C_bisim [in semantics.ccs.properties]
C_R [in semantics.ccs.properties]
C_limit [in semantics.tower.direct_induction]
C_step [in semantics.tower.direct_induction]
D
Def [in semantics.wp.ic]Do [in semantics.wp.gc]
E
ext_shift [in semantics.ccomega.typing]ext_bound [in semantics.ccomega.typing]
F
Fix [in semantics.ccs.syntax]Frame.Class [in semantics.ord.frame]
Frame.Mixin [in semantics.ord.frame]
Frame.Pack [in semantics.ord.frame]
I
If [in semantics.wp.ic]Inhab.tr [in semantics.base.inhab]
is_finite_ext [in semantics.ccomega.subjectreduction]
is_finite_empty [in semantics.ccomega.subjectreduction]
J
Jump [in semantics.wp.ic]L
lam [in semantics.f.fsyntax]lam [in semantics.debruijn.syntax]
lam [in semantics.ccomega.syntax]
lam [in semantics.f.fcbvsyntax]
LLat.Class [in semantics.tower.llat]
LLat.Mixin [in semantics.tower.llat]
LLat.Pack [in semantics.tower.llat]
M
mfun [in semantics.ord.mfun]mk_interval [in semantics.tower.reals]
mk_equiv [in semantics.base.overture]
mk_is_equiv [in semantics.base.overture]
mk_hprop [in semantics.base.overture]
mk_model [in semantics.f.types]
mk_lprop [in semantics.tower.llat]
mk_is_continuous [in semantics.ord.cont]
mk_fp [in semantics.tower.tarski]
mk_lts [in semantics.tower.ex_similarity]
mk_sieve [in semantics.ord.sheaf]
mk_sheaf [in semantics.ord.sheaf]
mk_basis_pred [in semantics.ord.sheaf]
N
New [in semantics.ccs.syntax]O
Ord.Class [in semantics.ord.ordtype]Ord.Mixin [in semantics.ord.ordtype]
Ord.Pack [in semantics.ord.ordtype]
P
Par [in semantics.ccs.syntax]Pataraia.T_limit [in semantics.tower.direct_induction]
Pataraia.T_step [in semantics.tower.direct_induction]
prod [in semantics.ccomega.syntax]
prop [in semantics.ccomega.sorts]
Pro.Mixin [in semantics.ord.protype]
Pro.Pack [in semantics.ord.protype]
pstep_prod [in semantics.ccomega.churchrosser]
pstep_lam [in semantics.ccomega.churchrosser]
pstep_app [in semantics.ccomega.churchrosser]
pstep_sort [in semantics.ccomega.churchrosser]
pstep_var [in semantics.ccomega.churchrosser]
pstep_beta [in semantics.ccomega.churchrosser]
R
RedProdSpecI [in semantics.ccomega.churchrosser]red_tapp [in semantics.f.fcbvreduction]
red_app [in semantics.f.fcbvreduction]
red_val [in semantics.f.fcbvreduction]
RI [in semantics.f.strongnorm]
S
Seq [in semantics.wp.gc]Skip [in semantics.wp.gc]
SNI [in semantics.ars]
starR [in semantics.ars]
starSE [in semantics.ars]
step_lam [in semantics.debruijn.reduction]
step_appR [in semantics.debruijn.reduction]
step_appL [in semantics.debruijn.reduction]
step_eta [in semantics.debruijn.reduction]
step_beta [in semantics.debruijn.reduction]
step_prodR [in semantics.ccomega.reduction]
step_prodL [in semantics.ccomega.reduction]
step_lam [in semantics.ccomega.reduction]
step_appR [in semantics.ccomega.reduction]
step_appL [in semantics.ccomega.reduction]
step_beta [in semantics.ccomega.reduction]
step_fix [in semantics.ccs.semantics]
step_restrict [in semantics.ccs.semantics]
step_comm [in semantics.ccs.semantics]
step_parr [in semantics.ccs.semantics]
step_parl [in semantics.ccs.semantics]
step_sumr [in semantics.ccs.semantics]
step_suml [in semantics.ccs.semantics]
step_act [in semantics.ccs.semantics]
step_tlam [in semantics.f.fsemantics]
step_lam [in semantics.f.fsemantics]
step_appR [in semantics.f.fsemantics]
step_appL [in semantics.f.fsemantics]
step_tbeta [in semantics.f.fsemantics]
step_beta [in semantics.f.fsemantics]
step_if_false [in semantics.wp.icsemantics]
step_if_true [in semantics.wp.icsemantics]
step_def [in semantics.wp.icsemantics]
step_act [in semantics.wp.icsemantics]
SubI [in semantics.ccomega.subtyping]
sub1_prod [in semantics.ccomega.subtyping]
sub1_sort [in semantics.ccomega.subtyping]
sub1_refl [in semantics.ccomega.subtyping]
Sum [in semantics.ccs.syntax]
T
tapp [in semantics.f.fsyntax]tapp [in semantics.f.fcbvsyntax]
tlam [in semantics.f.fsyntax]
tlam [in semantics.f.fcbvsyntax]
tvar [in semantics.f.types]
type [in semantics.ccomega.sorts]
ty_tlam [in semantics.f.weaknorm]
ty_lam [in semantics.f.weaknorm]
ty_var [in semantics.f.weaknorm]
ty_tapp [in semantics.f.weaknorm]
ty_app [in semantics.f.weaknorm]
ty_val [in semantics.f.weaknorm]
ty_tlam [in semantics.f.fsemantics]
ty_tapp [in semantics.f.fsemantics]
ty_lam [in semantics.f.fsemantics]
ty_app [in semantics.f.fsemantics]
ty_var [in semantics.f.fsemantics]
ty_sub [in semantics.ccomega.typing]
ty_prod [in semantics.ccomega.typing]
ty_lam [in semantics.ccomega.typing]
ty_app [in semantics.ccomega.typing]
ty_sort [in semantics.ccomega.typing]
ty_var [in semantics.ccomega.typing]
T_lim [in semantics.tower.tower]
T_step [in semantics.tower.tower]
U
univ [in semantics.ccomega.syntax]V
val [in semantics.f.fcbvsyntax]Var [in semantics.ccs.syntax]
var [in semantics.f.fsyntax]
var [in semantics.debruijn.syntax]
var [in semantics.ccomega.syntax]
var [in semantics.f.fcbvsyntax]
W
wlps_do [in semantics.wp.gcsemantics]wlps_case [in semantics.wp.gcsemantics]
wlps_seq [in semantics.wp.gcsemantics]
wlps_act [in semantics.wp.gcsemantics]
wlps_skip [in semantics.wp.gcsemantics]
wps_do_false [in semantics.wp.gcsemantics]
wps_do_true [in semantics.wp.gcsemantics]
wps_case [in semantics.wp.gcsemantics]
wps_seq [in semantics.wp.gcsemantics]
wps_act [in semantics.wp.gcsemantics]
wps_skip [in semantics.wp.gcsemantics]
Axiom Index
A
action [in semantics.wp.states]actionE [in semantics.wp.states]
action_eqP [in semantics.wp.states]
action_eq [in semantics.wp.states]
G
guard [in semantics.wp.states]guardE [in semantics.wp.states]
guard_eqP [in semantics.wp.states]
guard_eq [in semantics.wp.states]
I
Inhab.trP [in semantics.base.inhab]S
state [in semantics.wp.states]Inductive Index
A
accn [in semantics.ars]acc_on [in semantics.tower.linear_tower]
act [in semantics.ccs.syntax]
C
C [in semantics.ccs.properties]C [in semantics.tower.direct_induction]
cmd [in semantics.wp.gc]
conv [in semantics.ars]
conv [in semantics.base.quotient]
coverage [in semantics.ord.sheaf]
ctx_operator [in semantics.tower.ex_streams]
E
exp [in semantics.ccs.syntax]ext [in semantics.ccomega.typing]
H
has_type [in semantics.f.fsemantics]has_type [in semantics.ccomega.typing]
I
Inhab.inhab [in semantics.base.inhab]is_finite [in semantics.ccomega.subjectreduction]
P
Pataraia.T [in semantics.tower.direct_induction]pstep [in semantics.ccomega.churchrosser]
R
R [in semantics.f.strongnorm]red [in semantics.f.fcbvreduction]
RedProdSpec [in semantics.ccomega.churchrosser]
S
sn [in semantics.ars]sort [in semantics.ccomega.sorts]
star [in semantics.ars]
step [in semantics.debruijn.reduction]
step [in semantics.ccomega.reduction]
step [in semantics.ccs.semantics]
step [in semantics.f.fsemantics]
step [in semantics.wp.icsemantics]
sub [in semantics.ccomega.subtyping]
sub1 [in semantics.ccomega.subtyping]
T
T [in semantics.tower.tower]tm [in semantics.wp.ic]
tm [in semantics.f.fsyntax]
tm [in semantics.debruijn.syntax]
tm [in semantics.ccomega.syntax]
tm [in semantics.f.fcbvsyntax]
tm_has_type [in semantics.f.weaknorm]
ty [in semantics.f.types]
V
vl [in semantics.f.fcbvsyntax]vl_has_type [in semantics.f.weaknorm]
W
wlps [in semantics.wp.gcsemantics]wps [in semantics.wp.gcsemantics]
Projection Index
A
All [in semantics.f.types]Arr [in semantics.f.types]
B
basis_cov [in semantics.ord.sheaf]C
ccs_congruence_fix [in semantics.ccs.bisim]ccs_congruence_new [in semantics.ccs.bisim]
ccs_congruence_par [in semantics.ccs.bisim]
ccs_congruence_sum [in semantics.ccs.bisim]
chuL [in semantics.tower.llat]
chuR [in semantics.tower.llat]
CLat.base [in semantics.ord.clat]
CLat.inf [in semantics.ord.clat]
CLat.mixin [in semantics.ord.clat]
CLat.sort [in semantics.ord.clat]
contM [in semantics.ord.cont]
contT [in semantics.ord.cont]
cont_is_adjunction [in semantics.ord.cont]
E
equivmap [in semantics.base.overture]equivmap_is_equiv [in semantics.base.overture]
F
fpP [in semantics.tower.tarski]Frame.base [in semantics.ord.frame]
Frame.mixin [in semantics.ord.frame]
Frame.sort [in semantics.ord.frame]
H
hprop_is_prop [in semantics.base.overture]hprop_type [in semantics.base.overture]
I
interval_lower_lt_upper [in semantics.tower.reals]inverse [in semantics.base.overture]
inverse_cr [in semantics.base.overture]
inverse_cl [in semantics.base.overture]
L
LLat.base [in semantics.tower.llat]LLat.lt [in semantics.tower.llat]
LLat.mixin [in semantics.tower.llat]
LLat.sort [in semantics.tower.llat]
lmonoP [in semantics.tower.llat]
lmonotone_to_monotone [in semantics.tower.llat]
lower_uopen [in semantics.tower.reals]
lower_lset [in semantics.tower.reals]
lower_interval [in semantics.tower.reals]
lts_nodes [in semantics.tower.ex_similarity]
M
monofun [in semantics.ord.mfun]monotone_monofun [in semantics.ord.mfun]
O
Ord.base [in semantics.ord.ordtype]Ord.mixin [in semantics.ord.ordtype]
Ord.sort [in semantics.ord.ordtype]
P
Pataraia.infl_T [in semantics.tower.direct_induction]Pataraia.infl_dec [in semantics.tower.direct_induction]
Pataraia.infl_mono [in semantics.tower.direct_induction]
point [in semantics.tower.tarski]
presheaf_of_sheaf [in semantics.ord.sheaf]
Pro.rel [in semantics.ord.protype]
Pro.sort [in semantics.ord.protype]
R
radj_of_cont [in semantics.ord.cont]S
sievefun [in semantics.ord.sheaf]step [in semantics.tower.ex_similarity]
U
upper_lopen [in semantics.tower.reals]upper_uset [in semantics.tower.reals]
upper_interval [in semantics.tower.reals]
V
Var [in semantics.f.types]Section Index
A
AbstractPredTrans [in semantics.wp.abstract]AdjunctionsCLat [in semantics.ord.adj]
AdjunctionsFrame [in semantics.ord.adj]
AdjunctionsOrd [in semantics.ord.adj]
AdjunctionsOrdDual [in semantics.ord.adj]
AssociatedClosure [in semantics.tower.associated_closure]
B
BasisLaws [in semantics.ord.sheaf]C
CanonicalBasis [in semantics.ord.sheaf]CanonicalCoverage [in semantics.ord.sheaf]
Characterization [in semantics.tower.associated_closure]
Chu [in semantics.tower.llat]
ClassicalTower [in semantics.tower.linear_tower]
CLatDef [in semantics.ord.clat]
CLatLaws [in semantics.ord.clat]
CLat.ClassDef [in semantics.ord.clat]
ClosureCLat [in semantics.ord.adj]
ClosureOperatorsOrdType [in semantics.ord.adj]
ClosureOperatorsProType [in semantics.ord.adj]
CmdEqType [in semantics.wp.gc]
CmdInduction [in semantics.wp.gc]
CoFinal [in semantics.ars]
Commutation [in semantics.ars]
CompilerCorrectness [in semantics.wp.compiler]
CompilerCorrectness.Flatten [in semantics.wp.compiler]
ComputationN [in semantics.ars]
CongruenceProofs [in semantics.ccs.bisim]
ContCLat [in semantics.ord.cont]
ContFrame [in semantics.ord.cont]
ContinuousSup [in semantics.wp.prelim]
Coverage [in semantics.ord.sheaf]
D
Definitions [in semantics.ars]E
Equivalence [in semantics.base.overture]EquivalencePaths [in semantics.base.fext]
EquivProp [in semantics.base.overture]
Evaluation [in semantics.f.types]
F
FpCLat [in semantics.tower.tarski]FrameLaws [in semantics.ord.frame]
Frame.ClassDef [in semantics.ord.frame]
G
GCInduction [in semantics.wp.gc]GfpCompanion [in semantics.tower.gfp_companion]
GlbOrder [in semantics.ord.ordtype]
GlbPreorder [in semantics.ord.protype]
H
HoareRules [in semantics.wp.gcsemantics]I
InducedOrder [in semantics.ord.ordtype]InducedPreorder [in semantics.ord.protype]
InfClosedCoinduction [in semantics.tower.direct_induction]
Inhab.Induction [in semantics.base.inhab]
InjectiveSurjective [in semantics.base.inhab]
Interval [in semantics.base.fext]
IntervalDomain [in semantics.tower.reals]
IProdCLat [in semantics.ord.prod]
IProdFrame [in semantics.ord.prod]
IProdLLat [in semantics.tower.llat]
IProdOrdType [in semantics.ord.prod]
IProdProType [in semantics.ord.prod]
J
JLatLaws [in semantics.ord.clat]K
KernelOperationsOrder [in semantics.ord.adj]KernelOperators [in semantics.ord.adj]
Kleene [in semantics.wp.prelim]
L
LatLaws [in semantics.ord.clat]LeftAdjoints [in semantics.ord.adj]
LinearTower [in semantics.tower.linear_tower]
LLatLemmas [in semantics.tower.llat]
LLat.ClassDef [in semantics.tower.llat]
LubOrder [in semantics.ord.ordtype]
LubPreorder [in semantics.ord.protype]
M
MFun [in semantics.ord.mfun]MFunCLat [in semantics.ord.mfun]
MFunFrame [in semantics.ord.mfun]
MLatLaws [in semantics.ord.clat]
MonoCLat [in semantics.ord.mono]
O
Ord.ClassDef [in semantics.ord.ordtype]P
PairCLat [in semantics.ord.prod]PairFrame [in semantics.ord.prod]
PairOrdType [in semantics.ord.prod]
PairProType [in semantics.ord.prod]
ParameterizedTower [in semantics.tower.parameterized]
Pataraia.WithFunction [in semantics.tower.direct_induction]
PreorderLemmas [in semantics.ord.protype]
PresheafLaws [in semantics.ord.presheaf]
PresheafType [in semantics.ord.presheaf]
ProdCLat [in semantics.ord.prod]
PropInitial [in semantics.ord.prop]
PropOrder [in semantics.ord.prop]
Pro.ClassDef [in semantics.ord.protype]
PurePropositions [in semantics.ord.prop]
Q
QuotientMappingProperty [in semantics.base.quotient]QuotientTypes [in semantics.base.quotient]
QuotientTypes.Induction [in semantics.base.quotient]
QuotientTypes.Paths [in semantics.base.quotient]
R
ReverseCLat [in semantics.ord.clat]ReverseOrder [in semantics.ord.ordtype]
ReversePreorder [in semantics.ord.protype]
RightAdjoints [in semantics.ord.adj]
Rules [in semantics.ord.clat]
S
SheafCLat [in semantics.ord.sheaf]SheafFrame [in semantics.ord.sheaf]
Similarity [in semantics.tower.ex_similarity]
Streams [in semantics.tower.ex_streams]
SubcanonicalCoverage [in semantics.ord.sheaf]
SubcanonicalCoverageOrd [in semantics.ord.sheaf]
T
TarskiGfp [in semantics.tower.tarski]TarskiLfp [in semantics.tower.tarski]
Termination [in semantics.ars]
Tower [in semantics.tower.tower]
TowerCompanion [in semantics.tower.cocontinuous_tower]
Tower.DoubleInd [in semantics.tower.tower]
Tower.UptoLemma [in semantics.tower.tower]
Tower.UptoLemmaCharacterization [in semantics.tower.tower]
TruncationMappingProperty [in semantics.base.fext]
Y
Yoneda [in semantics.ord.presheaf]YonedaClat [in semantics.ord.presheaf]
YonedaOrd [in semantics.ord.presheaf]
Instance Index
A
act_proper_l [in semantics.ccs.bisim]act_proper [in semantics.ccs.bisim]
adj_monoR [in semantics.ord.adj]
adj_monoL [in semantics.ord.adj]
B
bisim_equiv [in semantics.ccs.bisim]bisim_rewrite [in semantics.ccs.bisim]
Bisim_mono [in semantics.ccs.bisim]
C
canonical_is_subcanonical [in semantics.ord.sheaf]ccs_congruence_bisim [in semantics.ccs.bisim]
closure_of_is_closure [in semantics.tower.associated_closure]
cont_is_adjunction_frame [in semantics.ord.cont]
co_mono [in semantics.tower.gfp_companion]
F
Fbisim_mono [in semantics.ccs.bisim]fix_proper [in semantics.ccs.bisim]
Fsim_mono [in semantics.ccs.bisim]
G
gfp_mono [in semantics.wp.compiler]I
impl_prop_subrelation [in semantics.ord.prop]imp_proper [in semantics.ord.frame]
is_kernel_counit [in semantics.ord.adj]
is_closure_kernel_rev [in semantics.ord.adj]
is_kernel_closure_rev [in semantics.ord.adj]
is_closure_unit [in semantics.ord.adj]
J
join_proper [in semantics.ord.clat]K
kleene_t_mono [in semantics.tower.cocontinuous_tower]L
lfp_mono [in semantics.wp.compiler]M
mceil_is_adjunction [in semantics.ord.mfun]meet_proper [in semantics.ord.clat]
mfloor_is_adjunction [in semantics.ord.mfun]
mfun_proper [in semantics.ord.mfun]
mfun_monotone [in semantics.ord.mfun]
monofun_is_proper [in semantics.ord.mfun]
monotone_yo [in semantics.ord.presheaf]
monotone_proper [in semantics.ord.mono]
monotone_kernel [in semantics.ord.adj]
monotone_closure [in semantics.ord.adj]
monotone_embed [in semantics.ord.sheaf]
N
new_proper [in semantics.ccs.bisim]O
obisim_equiv [in semantics.ccs.bisim]ord_op_preord [in semantics.ord.protype]
ord_op_trans [in semantics.ord.protype]
ord_op_refl [in semantics.ord.protype]
ord_op_rew [in semantics.ord.protype]
P
par_proper [in semantics.ccs.bisim]presheaf_of_sheaf_monotone [in semantics.ord.sheaf]
prod_pointwise_subrelation [in semantics.ord.prod]
proper_monotone [in semantics.ord.mono]
prop_impl_subrelation [in semantics.ord.prop]
pure_is_continuous [in semantics.ord.prop]
pure_is_adjunction [in semantics.ord.prop]
R
rev_is_adjunction [in semantics.ord.adj]S
sceil_mono [in semantics.ccs.bisim]sheafify_is_continuous [in semantics.ord.sheaf]
sheafify_adj_frame [in semantics.ord.sheaf]
sheafify_adj [in semantics.ord.sheaf]
shelve_monotone [in semantics.ord.mono]
sort_prod_proper [in semantics.ccomega.sorts]
sum_proper [in semantics.ccs.bisim]
T
t_monotone [in semantics.tower.tower]t_closure [in semantics.tower.tower]
U
upto_sum_o [in semantics.ccs.bisim]upto_act_open [in semantics.ccs.bisim]
upto_act [in semantics.ccs.bisim]
W
wlp_loop_mono [in semantics.wp.gcsemantics]wpF_mono [in semantics.wp.gcsemantics]
wpG_mono [in semantics.wp.gcsemantics]
wpI_mono [in semantics.wp.icsemantics]
wp_loop_mono [in semantics.wp.gcsemantics]
other
ε_mono [in semantics.tower.ex_streams]Abbreviation Index
B
bisim [in semantics.ccs.bisim]Bisim [in semantics.ccs.bisim]
C
CLat.Exports.CLat [in semantics.ord.clat]CLat.Exports.clat [in semantics.ord.clat]
CLat.Exports.CLatMixin [in semantics.ord.clat]
CLat.xclass [in semantics.ord.clat]
compile [in semantics.wp.compiler]
ctm [in semantics.f.weaknorm]
cvl [in semantics.f.weaknorm]
E
E [in semantics.f.strongnorm]F
Frame.Exports.Frame [in semantics.ord.frame]Frame.Exports.frame [in semantics.ord.frame]
Frame.Exports.FrameMixin [in semantics.ord.frame]
Frame.xclass [in semantics.ord.frame]
I
InducedOrdType [in semantics.ord.ordtype]InducedProType [in semantics.ord.protype]
K
K [in semantics.f.strongnorm]L
LLat.Exports.LLat [in semantics.tower.llat]LLat.Exports.llat [in semantics.tower.llat]
LLat.Exports.LLatMixin [in semantics.tower.llat]
LLat.xclass [in semantics.tower.llat]
M
mstep [in semantics.wp.icsemantics]O
obisim [in semantics.ccs.bisim]Ord.Exports.OrdMixin [in semantics.ord.ordtype]
Ord.Exports.OrdType [in semantics.ord.ordtype]
Ord.Exports.ordType [in semantics.ord.ordtype]
Ord.xclass [in semantics.ord.ordtype]
P
presheaf [in semantics.ord.presheaf]Pro.class_of [in semantics.ord.protype]
Pro.Exports.ProMixin [in semantics.ord.protype]
Pro.Exports.ProType [in semantics.ord.protype]
Pro.Exports.proType [in semantics.ord.protype]
R
rbisim [in semantics.tower.ex_streams]red [in semantics.ccomega.reduction]
ren [in semantics.ccs.syntax]
T
t [in semantics.tower.parameterized]T [in semantics.tower.cocontinuous_tower]
T [in semantics.tower.linear_tower]
T [in semantics.tower.direct_induction]
V
V [in semantics.f.strongnorm]Definition Index
A
accn_ind' [in semantics.ars]active [in semantics.f.strongnorm]
all2 [in semantics.wp.gc]
antisymmetric [in semantics.base.overture]
ap [in semantics.base.overture]
asimpl [in semantics.ccs.syntax]
B
basis [in semantics.ord.sheaf]bijective_equiv [in semantics.base.inhab]
bisim [in semantics.tower.ex_streams]
bot [in semantics.ord.clat]
bound [in semantics.data.fintype]
C
C [in semantics.f.strongnorm]canonical [in semantics.ord.sheaf]
cempty [in semantics.ccomega.subjectreduction]
cexp [in semantics.ccs.semantics]
chain [in semantics.tower.cocontinuous_tower]
chu_lt [in semantics.tower.llat]
chu_inf [in semantics.tower.llat]
chu_le [in semantics.tower.llat]
classic [in semantics.tower.linear_tower]
classical_lt [in semantics.tower.linear_tower]
CLat.class [in semantics.ord.clat]
CLat.clone [in semantics.ord.clat]
CLat.ordType [in semantics.ord.clat]
CLat.pack [in semantics.ord.clat]
CLat.proType [in semantics.ord.clat]
closure_to_inf_closed [in semantics.tower.associated_closure]
closure_of [in semantics.tower.associated_closure]
cmd_eq [in semantics.wp.gc]
cmd_ind' [in semantics.wp.gc]
cmorph [in semantics.ccomega.contextmorphism]
co [in semantics.tower.gfp_companion]
codirected [in semantics.tower.cocontinuous_tower]
codirected [in semantics.tower.direct_induction]
cofinal [in semantics.ars]
com [in semantics.ars]
comp [in semantics.wp.compiler]
compatible [in semantics.tower.tower]
conf [in semantics.wp.icsemantics]
confluent [in semantics.ars]
constant [in semantics.base.fext]
context_ok [in semantics.ccomega.typing]
continuous [in semantics.wp.abstract]
continuous [in semantics.wp.gcsemantics]
countable_branching [in semantics.tower.ex_similarity]
Cover [in semantics.ord.sheaf]
coverage_sheafify [in semantics.ord.sheaf]
cover_le [in semantics.ord.sheaf]
CR [in semantics.ars]
ctx [in semantics.ccomega.typing]
D
D [in semantics.f.weaknorm]D [in semantics.f.strongnorm]
deterministic [in semantics.wp.abstract]
deterministic [in semantics.wp.icsemantics]
diamond [in semantics.ars]
directed [in semantics.tower.direct_induction]
distributes_over [in semantics.wp.abstract]
distributive [in semantics.wp.abstract]
dual [in semantics.ccs.semantics]
E
E [in semantics.f.weaknorm]embed [in semantics.ord.sheaf]
equiv_inverse [in semantics.base.overture]
eval [in semantics.f.types]
evaln [in semantics.ars]
F
Fbisim [in semantics.ccs.bisim]fext [in semantics.base.fext]
fin [in semantics.data.fintype]
flatmap [in semantics.wp.compiler]
flip [in semantics.ccs.bisim]
fp_inf [in semantics.tower.tarski]
Frame.class [in semantics.ord.frame]
Frame.clat [in semantics.ord.frame]
Frame.clone [in semantics.ord.frame]
Frame.ordType [in semantics.ord.frame]
Frame.pack [in semantics.ord.frame]
Frame.proType [in semantics.ord.frame]
Fsim [in semantics.ccs.bisim]
G
gc [in semantics.wp.gc]gc_ind [in semantics.wp.gc]
gc_ind' [in semantics.wp.gc]
gfp [in semantics.tower.tarski]
gfp_below [in semantics.tower.tarski]
Gtest [in semantics.wp.gcsemantics]
gtest [in semantics.wp.gcsemantics]
guard [in semantics.ccs.semantics]
H
has_type_ind [in semantics.f.weaknorm]hex [in semantics.base.inhab]
hex_rec_prop [in semantics.base.inhab]
hex_ind [in semantics.base.inhab]
hex_rec [in semantics.base.inhab]
hex_rect [in semantics.base.inhab]
hpropP [in semantics.base.overture]
I
ids [in semantics.ccs.syntax]imp [in semantics.ord.frame]
induced_le [in semantics.ord.protype]
inf [in semantics.ord.clat]
infguard [in semantics.ord.clat]
inf_closed_to_closure [in semantics.tower.associated_closure]
inf_closed [in semantics.ord.clat]
inhab_indP [in semantics.base.inhab]
inhab_ind [in semantics.base.inhab]
inhab_rec [in semantics.base.inhab]
inhab_map_is_equiv [in semantics.base.fext]
inhab_map [in semantics.base.fext]
Inhab.inhab_rect [in semantics.base.inhab]
inst [in semantics.wp.ic]
inst [in semantics.f.fsyntax]
inst [in semantics.debruijn.syntax]
inst [in semantics.ccomega.syntax]
interior [in semantics.tower.reals]
interval [in semantics.base.fext]
interval_lt [in semantics.tower.reals]
interval_inf [in semantics.tower.reals]
interval_le [in semantics.tower.reals]
inverse_cand [in semantics.base.inhab]
in_class [in semantics.base.quotient]
iprod [in semantics.base.overture]
iprod_inf [in semantics.ord.prod]
iprod_le [in semantics.ord.prod]
iprod_lt [in semantics.tower.llat]
is_glb [in semantics.ord.protype]
is_lb [in semantics.ord.protype]
is_lub [in semantics.ord.protype]
is_ub [in semantics.ord.protype]
is_equiv_comp [in semantics.base.overture]
is_equiv_inv [in semantics.base.overture]
is_equiv_idfun [in semantics.base.overture]
is_prop [in semantics.base.overture]
is_type [in semantics.ccomega.typing]
is_cocontinuous [in semantics.tower.cocontinuous_tower]
is_kernel [in semantics.ord.adj]
is_closure [in semantics.ord.adj]
is_adjunction [in semantics.ord.adj]
is_subcanonical [in semantics.ord.sheaf]
is_sheaf [in semantics.ord.sheaf]
J
J [in semantics.base.overture]join [in semantics.ord.clat]
joinable [in semantics.ars]
K
K [in semantics.base.pext]kleene_t [in semantics.tower.cocontinuous_tower]
L
L [in semantics.f.weaknorm]LetDef [in semantics.wp.compiler]
lfp [in semantics.tower.tarski]
lfp_approx [in semantics.wp.icsemantics]
lfp_above [in semantics.tower.tarski]
lift [in semantics.f.types]
LLat.class [in semantics.tower.llat]
LLat.clat [in semantics.tower.llat]
LLat.clone [in semantics.tower.llat]
LLat.ordType [in semantics.tower.llat]
LLat.pack [in semantics.tower.llat]
LLat.proType [in semantics.tower.llat]
loop [in semantics.tower.ex_similarity]
lts [in semantics.ccs.semantics]
M
M [in semantics.f.strongnorm]map_quot [in semantics.base.quotient]
map_inhab [in semantics.base.fext]
mceil [in semantics.ord.mfun]
meet [in semantics.ord.clat]
mfloor [in semantics.ord.mfun]
mfun_inf [in semantics.ord.mfun]
mfun_of [in semantics.ord.mfun]
mk_mfun [in semantics.ord.mfun]
monotone [in semantics.ord.mono]
N
nat_le [in semantics.ccomega.sorts]neq [in semantics.tower.ex_streams]
nf [in semantics.ars]
NGtest [in semantics.wp.gcsemantics]
normal [in semantics.ars]
normalizing [in semantics.ars]
nsim [in semantics.tower.ex_similarity]
null [in semantics.data.fintype]
O
OBisim [in semantics.ccs.bisim]observable [in semantics.ccs.semantics]
ord_op [in semantics.ord.protype]
ord_l_op [in semantics.tower.llat]
Ord.class [in semantics.ord.ordtype]
Ord.clone [in semantics.ord.ordtype]
Ord.pack [in semantics.ord.ordtype]
Ord.proType [in semantics.ord.ordtype]
P
pack_induced_ordType [in semantics.ord.ordtype]pack_induced_proType [in semantics.ord.protype]
pairb [in semantics.base.fext]
pair_inf [in semantics.ord.prod]
pair_le [in semantics.ord.prod]
Pataraia.infl_null [in semantics.tower.direct_induction]
Pataraia.ν [in semantics.tower.direct_induction]
path_I [in semantics.base.fext]
Pred [in semantics.base.overture]
presheaf_of [in semantics.ord.presheaf]
presheaf_type [in semantics.ord.presheaf]
prop_inf [in semantics.ord.prop]
prop_le [in semantics.ord.prop]
prop_equiv [in semantics.base.overture]
prop_is_equiv [in semantics.base.overture]
Pro.class [in semantics.ord.protype]
Pro.clone [in semantics.ord.protype]
Pro.pack [in semantics.ord.protype]
psstep [in semantics.ccomega.churchrosser]
pt [in semantics.wp.gcsemantics]
ptn [in semantics.wp.icsemantics]
ptrans [in semantics.wp.abstract]
pure [in semantics.ord.prop]
Q
quot [in semantics.base.quotient]quot_map_is_equiv [in semantics.base.quotient]
quot_map [in semantics.base.quotient]
quot_rec2 [in semantics.base.quotient]
quot_ind [in semantics.base.quotient]
quot_rect [in semantics.base.quotient]
quot_rect_total_id [in semantics.base.quotient]
quot_rect_total [in semantics.base.quotient]
quot_rec [in semantics.base.quotient]
R
rbind [in semantics.ccs.syntax]rcomp [in semantics.ccs.syntax]
reducible [in semantics.ars]
reflexive [in semantics.base.overture]
Rel [in semantics.base.overture]
ren [in semantics.data.fintype]
rename [in semantics.f.fsyntax]
rename [in semantics.debruijn.syntax]
rename [in semantics.ccomega.syntax]
ren_compat [in semantics.wp.icsemantics]
repr [in semantics.base.quotient]
respectful [in semantics.tower.tower]
restrict [in semantics.ord.sheaf]
reverse [in semantics.ord.protype]
rev_le [in semantics.ord.protype]
rev_inf [in semantics.ord.clat]
rho [in semantics.ccomega.churchrosser]
right_adjoint_proj [in semantics.ord.adj]
rinst [in semantics.wp.ic]
rmap [in semantics.ccs.syntax]
S
SA [in semantics.tower.ex_streams]sceil [in semantics.ccs.bisim]
scons [in semantics.data.fintype]
sconv [in semantics.ccomega.reduction]
sheafify [in semantics.ord.sheaf]
sheaf_imp [in semantics.ord.sheaf]
sheaf_inf [in semantics.ord.sheaf]
shift [in semantics.data.fintype]
sieve_bot [in semantics.ord.sheaf]
sieve_top [in semantics.ord.sheaf]
sigT_eq_pr2 [in semantics.base.overture]
sigT_eq_pr1 [in semantics.base.overture]
sim [in semantics.tower.ex_similarity]
similar [in semantics.tower.ex_similarity]
simple [in semantics.wp.compiler]
sort_succ [in semantics.ccomega.sorts]
sort_prod [in semantics.ccomega.sorts]
sort_le [in semantics.ccomega.sorts]
sound_up_to [in semantics.tower.parameterized]
sred [in semantics.ccomega.reduction]
stream_companion [in semantics.tower.ex_streams]
subst [in semantics.wp.ic]
subst [in semantics.f.fsyntax]
subst [in semantics.debruijn.syntax]
subst [in semantics.ccomega.syntax]
sup [in semantics.ord.clat]
supguard [in semantics.ord.clat]
sup_closed [in semantics.ord.clat]
surjective [in semantics.base.inhab]
symmetric [in semantics.base.overture]
T
t [in semantics.tower.tower]terminates [in semantics.wp.icsemantics]
Tm_has_type [in semantics.f.weaknorm]
tm_has_type_ind [in semantics.f.weaknorm]
tm_inst [in semantics.f.fcbvsyntax]
tm_rename [in semantics.f.fcbvsyntax]
tm_ind [in semantics.f.fcbvsyntax]
top [in semantics.ord.clat]
tpred [in semantics.f.strongnorm]
transitive [in semantics.base.overture]
transport [in semantics.base.overture]
triangle [in semantics.ars]
triple [in semantics.wp.gcsemantics]
tripleG [in semantics.wp.gcsemantics]
tup [in semantics.f.types]
tv_ind [in semantics.f.fcbvsyntax]
tyinst [in semantics.f.types]
tyrename [in semantics.f.types]
tysubst [in semantics.f.types]
U
unembed [in semantics.ord.sheaf]unify [in semantics.base.meta]
up [in semantics.data.fintype]
upi [in semantics.wp.ic]
upi [in semantics.ccs.syntax]
upi [in semantics.f.fsyntax]
upi [in semantics.debruijn.syntax]
upi [in semantics.ccomega.syntax]
V
V [in semantics.f.weaknorm]Vl_has_type [in semantics.f.weaknorm]
vl_has_type_ind [in semantics.f.weaknorm]
vl_inst [in semantics.f.fcbvsyntax]
vl_rename [in semantics.f.fcbvsyntax]
vl_ind [in semantics.f.fcbvsyntax]
vsubst [in semantics.f.fcbvsyntax]
vup [in semantics.f.fcbvsyntax]
W
weakly_guarded [in semantics.ccs.properties]wlp [in semantics.wp.abstract]
wlp [in semantics.wp.gcsemantics]
wlpi [in semantics.wp.icsemantics]
wlp_loop [in semantics.wp.gcsemantics]
wn [in semantics.ars]
wp [in semantics.wp.abstract]
wp [in semantics.wp.gcsemantics]
wpF [in semantics.wp.gcsemantics]
wpG [in semantics.wp.gcsemantics]
wpi [in semantics.wp.icsemantics]
wpI [in semantics.wp.icsemantics]
wpi_distributive [in semantics.wp.icsemantics]
wp_distributive [in semantics.wp.gcsemantics]
wp_loop [in semantics.wp.gcsemantics]
Y
yo [in semantics.ord.presheaf]other
Ω [in semantics.wp.ic]ε [in semantics.tower.ex_streams]
ν [in semantics.tower.gfp_companion]
Record Index
B
basis_pred [in semantics.ord.sheaf]C
CcsCongruence [in semantics.ccs.bisim]CLat.class_of [in semantics.ord.clat]
CLat.mixin_of [in semantics.ord.clat]
CLat.type [in semantics.ord.clat]
E
equiv [in semantics.base.overture]F
fp [in semantics.tower.tarski]Frame.class_of [in semantics.ord.frame]
Frame.mixin_of [in semantics.ord.frame]
Frame.type [in semantics.ord.frame]
H
hprop [in semantics.base.overture]I
interval [in semantics.tower.reals]is_equiv [in semantics.base.overture]
is_continuous [in semantics.ord.cont]
L
LLat.class_of [in semantics.tower.llat]LLat.mixin_of [in semantics.tower.llat]
LLat.type [in semantics.tower.llat]
lmonotone [in semantics.tower.llat]
lprop [in semantics.tower.llat]
lts [in semantics.tower.ex_similarity]
M
mfun_type [in semantics.ord.mfun]model [in semantics.f.types]
O
Ord.class_of [in semantics.ord.ordtype]Ord.mixin_of [in semantics.ord.ordtype]
Ord.type [in semantics.ord.ordtype]
P
Pataraia.infl [in semantics.tower.direct_induction]Pro.mixin_of [in semantics.ord.protype]
Pro.type [in semantics.ord.protype]
S
sheaf [in semantics.ord.sheaf]sieve [in semantics.ord.sheaf]
| 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 | (2105 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 | (62 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 | (12 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 | (238 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 | (63 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 | (881 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 | (172 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 | (10 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (43 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 | (57 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 | (113 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 | (68 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 | (40 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 | (316 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 | (30 entries) |