| 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 | (2070 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 | (106 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 | (149 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 | (26 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 | (595 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 | (266 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 | (96 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 | (144 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 | (96 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 | (48 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 | (69 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 | (20 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 | (399 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 | (56 entries) |
Global Index
A
AddEndofunctors [module, in interfaces.FunctorCategory]AddEndofunctors.End [module, in interfaces.FunctorCategory]
AddEndofunctors.EndNotations [module, in interfaces.FunctorCategory]
_ ∘ _ (hom_scope) [notation, in interfaces.FunctorCategory]
_ ∘ _ (obj_scope) [notation, in interfaces.FunctorCategory]
AddOp [module, in interfaces.Category]
AddOp.Op [module, in interfaces.Category]
AdjoinBot [library]
all_eq_none [lemma, in models.IntStrat]
all_eq_some [lemma, in models.IntStrat]
amap [definition, in models.Signature]
amap_compose [lemma, in models.Signature]
amap_id [lemma, in models.Signature]
application [record, in models.Signature]
application [record, in models.IntStrat]
apply [constructor, in models.Signature]
app_coh [lemma, in models.Coherence]
ar [projection, in models.Signature]
ar [projection, in models.IntStrat]
assert [definition, in examples.CAL]
assert_r [lemma, in examples.CAL]
assert_l [lemma, in examples.CAL]
assert_true [lemma, in examples.CAL]
B
basis [definition, in models.Signature]basis_hmap [lemma, in models.Signature]
bcomp [definition, in models.IntStrat]
bcomp_bcomp [lemma, in models.IntStrat]
bcomp_bid_r [lemma, in models.IntStrat]
bcomp_bid_l [lemma, in models.IntStrat]
bid [definition, in models.IntStrat]
Bifunctor [module, in interfaces.Functor]
BifunctorDefinition [module, in interfaces.Functor]
BifunctorDefinition.fmap [axiom, in interfaces.Functor]
BifunctorDefinition.fmap_compose [axiom, in interfaces.Functor]
BifunctorDefinition.fmap_id [axiom, in interfaces.Functor]
BifunctorDefinition.omap [axiom, in interfaces.Functor]
BifunctorTheory [module, in interfaces.Functor]
BifunctorTheory.fmap_iso [definition, in interfaces.Functor]
BifunctorTheory.PC [module, in interfaces.Functor]
BifunctorTheory.PF [module, in interfaces.Functor]
BifunctorTheory.PF.fmap [definition, in interfaces.Functor]
BifunctorTheory.PF.fmap_compose [lemma, in interfaces.Functor]
BifunctorTheory.PF.fmap_id [lemma, in interfaces.Functor]
BifunctorTheory.PF.omap [definition, in interfaces.Functor]
bigop_eq [instance, in models.IntSpec]
bijection [record, in models.IntStrat]
bij_lens_bcomp [lemma, in models.IntStrat]
bij_lens [definition, in models.IntStrat]
bij_eq_ext [lemma, in models.IntStrat]
bind [projection, in structures.Monad]
bind_inf [projection, in structures.Monad]
bind_sup [projection, in structures.Monad]
bind_bind [projection, in structures.Monad]
bind_ret [projection, in structures.Monad]
bot [definition, in structures.Lattice]
bot [definition, in models.Coherence]
bot_lb [lemma, in structures.Lattice]
bot_ref [lemma, in models.Coherence]
bq_rb_correct [lemma, in examples.CAL]
bq_rb_intro [constructor, in examples.CAL]
bq_state [definition, in examples.CAL]
bq_sig [inductive, in examples.CAL]
bw [projection, in models.IntStrat]
bw_fw [projection, in models.IntStrat]
C
CAL [library]CALspec [definition, in examples.CAL]
CALspec_mor [definition, in examples.CAL]
Cartesian [module, in interfaces.MonoidalCategory]
CartesianCategory [module, in interfaces.MonoidalCategory]
CartesianDefinition [module, in interfaces.MonoidalCategory]
CartesianDefinition.Prod [module, in interfaces.MonoidalCategory]
CartesianFromProducts [module, in interfaces.Limits]
CartesianFromProducts.Prod [module, in interfaces.Limits]
CartesianStructure [module, in interfaces.MonoidalCategory]
CartesianStructureDefinition [module, in interfaces.MonoidalCategory]
CartesianStructureDefinition.omap [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.pair [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.pair_pi_compose [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.p1 [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.p1_pair [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.p2 [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.p2_pair [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.ter [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.ter_uni [axiom, in interfaces.MonoidalCategory]
CartesianStructureDefinition.unit [axiom, in interfaces.MonoidalCategory]
CartesianStructureFromProducts [module, in interfaces.Limits]
CartesianStructureFromProducts.omap [definition, in interfaces.Limits]
CartesianStructureFromProducts.pair [definition, in interfaces.Limits]
CartesianStructureFromProducts.pair_pi_compose [lemma, in interfaces.Limits]
CartesianStructureFromProducts.p1 [definition, in interfaces.Limits]
CartesianStructureFromProducts.p1_pair [lemma, in interfaces.Limits]
CartesianStructureFromProducts.p2 [definition, in interfaces.Limits]
CartesianStructureFromProducts.p2_pair [lemma, in interfaces.Limits]
CartesianStructureFromProducts.ter [definition, in interfaces.Limits]
CartesianStructureFromProducts.ter_uni [lemma, in interfaces.Limits]
CartesianStructureFromProducts.unit [definition, in interfaces.Limits]
CartesianStructureLimit [module, in interfaces.Limits]
CartesianStructureLimit.prod_c_lim [instance, in interfaces.Limits]
CartesianStructureLimit.prod_c [definition, in interfaces.Limits]
CartesianStructureLimit.prod_d [definition, in interfaces.Limits]
CartesianStructureTheory [module, in interfaces.MonoidalCategory]
CartesianStructureTheory.assoc [definition, in interfaces.MonoidalCategory]
CartesianStructureTheory.assoc_coh [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.assoc_nat [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.fmap [definition, in interfaces.MonoidalCategory]
CartesianStructureTheory.fmap_compose [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.fmap_id [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.lunit [definition, in interfaces.MonoidalCategory]
CartesianStructureTheory.lunit_nat [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.pair_compose [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.pair_pi [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.pair_uni [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.p1_pair_rewrite [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.p2_pair_rewrite [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.runit [definition, in interfaces.MonoidalCategory]
CartesianStructureTheory.runit_swap [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.runit_nat [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.swap [definition, in interfaces.MonoidalCategory]
CartesianStructureTheory.swap_swap [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.swap_assoc [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.swap_nat [lemma, in interfaces.MonoidalCategory]
CartesianStructureTheory.unit_coh [lemma, in interfaces.MonoidalCategory]
_ & _ (hom_scope) [notation, in interfaces.MonoidalCategory]
_ & _ (obj_scope) [notation, in interfaces.MonoidalCategory]
CartesianTheory [module, in interfaces.MonoidalCategory]
CartesianTheory.T [abbreviation, in interfaces.MonoidalCategory]
_ && _ (hom_scope) [notation, in interfaces.MonoidalCategory]
_ && _ (obj_scope) [notation, in interfaces.MonoidalCategory]
Category [record, in structures.Category]
Category [module, in interfaces.Category]
Category [library]
Category [library]
CategoryDefinition [module, in interfaces.Category]
CategoryDefinition.compose [axiom, in interfaces.Category]
CategoryDefinition.compose_assoc [axiom, in interfaces.Category]
CategoryDefinition.compose_id_right [axiom, in interfaces.Category]
CategoryDefinition.compose_id_left [axiom, in interfaces.Category]
CategoryDefinition.id [axiom, in interfaces.Category]
CategoryDefinition.m [axiom, in interfaces.Category]
CategoryDefinition.t [axiom, in interfaces.Category]
CategoryTheory [module, in interfaces.Category]
CategoryTheory.bw [projection, in interfaces.Category]
CategoryTheory.bw_iso [definition, in interfaces.Category]
CategoryTheory.bw_fw_rewrite [lemma, in interfaces.Category]
CategoryTheory.bw_fw [projection, in interfaces.Category]
CategoryTheory.compose_bw_l_eq [lemma, in interfaces.Category]
CategoryTheory.compose_fw_l_eq [lemma, in interfaces.Category]
CategoryTheory.compose_iso [definition, in interfaces.Category]
CategoryTheory.eq_fw_bw_r_2 [lemma, in interfaces.Category]
CategoryTheory.eq_fw_bw_l_2 [lemma, in interfaces.Category]
CategoryTheory.eq_fw_bw_r_1 [lemma, in interfaces.Category]
CategoryTheory.eq_fw_bw_l_1 [lemma, in interfaces.Category]
CategoryTheory.fw [projection, in interfaces.Category]
CategoryTheory.fw_bw_rewrite [lemma, in interfaces.Category]
CategoryTheory.fw_bw [projection, in interfaces.Category]
CategoryTheory.id_iso [definition, in interfaces.Category]
CategoryTheory.iso [record, in interfaces.Category]
CategoryTheory.iso_eq_fw_bw [lemma, in interfaces.Category]
CategoryTheory.iso_eq_bw [lemma, in interfaces.Category]
CategoryTheory.iso_eq_fw [lemma, in interfaces.Category]
_ @ _ (hom_scope) [notation, in interfaces.Category]
_ ~~> _ (type_scope) [notation, in interfaces.Category]
CategoryWithEndofunctors [module, in interfaces.FunctorCategory]
CategoryWithOp [module, in interfaces.Category]
ccpos [inductive, in models.IntStrat]
ccpos_suspended [constructor, in models.IntStrat]
ccpos_right [constructor, in models.IntStrat]
ccpos_mid [constructor, in models.IntStrat]
ccpos_left [constructor, in models.IntStrat]
ccpos_ready [constructor, in models.IntStrat]
CDCat [record, in structures.Category]
cdcat_cat [projection, in structures.Category]
CDL [module, in lattices.FCD]
cdlattice [record, in structures.Lattice]
cdlat_prod [definition, in lattices.LatticeProduct]
cdl_poset [projection, in structures.Lattice]
CDL.cmor_inf [instance, in lattices.FCD]
CDL.cmor_sup [instance, in lattices.FCD]
CDL.compose_mor [lemma, in lattices.FCD]
CDL.DEF [section, in lattices.FCD]
CDL.id_mor [lemma, in lattices.FCD]
CDL.mor [projection, in lattices.FCD]
CDL.mor [constructor, in lattices.FCD]
CDL.Morphism [record, in lattices.FCD]
CDL.Morphism [inductive, in lattices.FCD]
CDL.mor_ref [instance, in lattices.FCD]
CDMonad [record, in structures.Monad]
cepos [inductive, in models.IntStrat]
cepos_suspended [constructor, in models.IntStrat]
cepos_ready [constructor, in models.IntStrat]
clique [record, in models.Coherence]
Cocartesian [module, in interfaces.MonoidalCategory]
CocartesianCategory [module, in interfaces.MonoidalCategory]
CocartesianDefinition [module, in interfaces.MonoidalCategory]
CocartesianDefinition.Plus [module, in interfaces.MonoidalCategory]
CocartesianStructure [module, in interfaces.MonoidalCategory]
CocartesianStructureDefinition [module, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair_iota_compose [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair_i2 [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair_i1 [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.ini [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.ini_uni [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.i1 [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.i2 [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.omap [axiom, in interfaces.MonoidalCategory]
CocartesianStructureDefinition.unit [axiom, in interfaces.MonoidalCategory]
CocartesianStructureTheory [module, in interfaces.MonoidalCategory]
CocartesianStructureTheory.assoc [definition, in interfaces.MonoidalCategory]
CocartesianStructureTheory.assoc_coh [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.assoc_nat [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_compose [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_iota [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_uni [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_i2_rewrite [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_i1_rewrite [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.fmap [definition, in interfaces.MonoidalCategory]
CocartesianStructureTheory.fmap_compose [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.fmap_id [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.lunit [definition, in interfaces.MonoidalCategory]
CocartesianStructureTheory.lunit_nat [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.runit [definition, in interfaces.MonoidalCategory]
CocartesianStructureTheory.runit_swap [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.runit_nat [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap [definition, in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap_swap [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap_assoc [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap_nat [lemma, in interfaces.MonoidalCategory]
CocartesianStructureTheory.unit_coh [lemma, in interfaces.MonoidalCategory]
_ + _ (hom_scope) [notation, in interfaces.MonoidalCategory]
_ + _ (obj_scope) [notation, in interfaces.MonoidalCategory]
CocartesianTheory [module, in interfaces.MonoidalCategory]
_ + _ (hom_scope) [notation, in interfaces.MonoidalCategory]
_ + _ (obj_scope) [notation, in interfaces.MonoidalCategory]
0 [notation, in interfaces.MonoidalCategory]
coh [projection, in models.Coherence]
Coherence [library]
coh_symm [projection, in models.Coherence]
coh_refl [projection, in models.Coherence]
Colimits [module, in interfaces.Limits]
combine_ans [definition, in models.IntStrat]
Completion [library]
compose [projection, in structures.Category]
compose [abbreviation, in models.IntStrat]
COMPOSE [section, in models.IntStrat]
compose_mor_l [projection, in structures.Category]
compose_mor_r [projection, in structures.Category]
compose_assoc [projection, in structures.Category]
compose_id [projection, in structures.Category]
compose_fcomp_has [lemma, in models.IntStrat]
COMPOSE_FCOMP [section, in models.IntStrat]
compose_assoc [lemma, in models.IntStrat]
compose_assoc_when [lemma, in models.IntStrat]
COMPOSE_COMPOSE [section, in models.IntStrat]
compose_id_r [lemma, in models.IntStrat]
compose_id_r_when [lemma, in models.IntStrat]
compose_id_has_r_lt [lemma, in models.IntStrat]
compose_id_has_r_gt [lemma, in models.IntStrat]
compose_id_l [lemma, in models.IntStrat]
compose_id_l_when [lemma, in models.IntStrat]
compose_id_has_l_lt [lemma, in models.IntStrat]
compose_id_has_l_gt [lemma, in models.IntStrat]
COMPOSE_ID [section, in models.IntStrat]
compose_next_la [lemma, in models.IntStrat]
compose_next_ra [lemma, in models.IntStrat]
compose_next_oa [lemma, in models.IntStrat]
compose_next_rq [lemma, in models.IntStrat]
compose_next_lq [lemma, in models.IntStrat]
compose_next_oq [lemma, in models.IntStrat]
compose_deterministic [instance, in models.IntStrat]
compose_when [definition, in models.IntStrat]
comp_has_assoc_2 [lemma, in models.IntStrat]
comp_has_assoc_1 [lemma, in models.IntStrat]
comp_has_pref [lemma, in models.IntStrat]
comp_la [constructor, in models.IntStrat]
comp_ra [constructor, in models.IntStrat]
comp_oa [constructor, in models.IntStrat]
comp_suspended [constructor, in models.IntStrat]
comp_rq [constructor, in models.IntStrat]
comp_lq [constructor, in models.IntStrat]
comp_oq [constructor, in models.IntStrat]
comp_ready [constructor, in models.IntStrat]
comp_has [inductive, in models.IntStrat]
ConcreteCategory [module, in interfaces.ConcreteCategory]
ConcreteCategory [library]
ConcreteCategoryDefinition [module, in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.compose_mor [axiom, in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.id_mor [axiom, in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.Morphism [axiom, in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.Structure [axiom, in interfaces.ConcreteCategory]
ConcreteCategoryTheory [module, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.apply [projection, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.carrier [projection, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.compose [definition, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.compose_assoc [lemma, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.compose_id_right [lemma, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.compose_id_left [lemma, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.id [definition, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.m [definition, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.meq [lemma, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.mkm [constructor, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.mkt [constructor, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.morphism [projection, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.structure [projection, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.structured_map [record, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.structured_set [record, in interfaces.ConcreteCategory]
ConcreteCategoryTheory.t [definition, in interfaces.ConcreteCategory]
cons [constructor, in models.Sets]
cons_coh [constructor, in models.Coherence]
conv [definition, in models.IntStrat]
conv_has_forbid_cont [lemma, in models.IntStrat]
conv_has_forbid_allow [lemma, in models.IntStrat]
conv_has_cont_allow [lemma, in models.IntStrat]
copair [definition, in models.Coherence]
copair_uniq [lemma, in models.Coherence]
copair_csi2 [lemma, in models.Coherence]
copair_csi1 [lemma, in models.Coherence]
Coproducts [module, in interfaces.Limits]
CoproductsDefinition [module, in interfaces.Limits]
CoproductsDefinition.coprod [axiom, in interfaces.Limits]
CoproductsDefinition.cotuple [axiom, in interfaces.Limits]
CoproductsDefinition.cotuple_iota [axiom, in interfaces.Limits]
CoproductsDefinition.iota [axiom, in interfaces.Limits]
CoproductsDefinition.iota_cotuple [axiom, in interfaces.Limits]
CoproductsTheory [module, in interfaces.Limits]
CoproductsTheory.cotuple_uni [lemma, in interfaces.Limits]
CoproductsTheory.cotuple_iota_rewrite [lemma, in interfaces.Limits]
cpos [inductive, in models.IntStrat]
cpos_suspended [constructor, in models.IntStrat]
cpos_right [constructor, in models.IntStrat]
cpos_left [constructor, in models.IntStrat]
cpos_ready [constructor, in models.IntStrat]
cSET [module, in interfaces.ConcreteCategory]
cSET.compose_mor [instance, in interfaces.ConcreteCategory]
cSET.id_mor [instance, in interfaces.ConcreteCategory]
cSET.Morphism [definition, in interfaces.ConcreteCategory]
cSET.Structure [definition, in interfaces.ConcreteCategory]
csi1 [definition, in models.Coherence]
csi2 [definition, in models.Coherence]
cspair [definition, in models.Coherence]
cspair_uniq [lemma, in models.Coherence]
cspair_csp2 [lemma, in models.Coherence]
cspair_csp1 [lemma, in models.Coherence]
csprod [definition, in models.Coherence]
csprod_coh [inductive, in models.Coherence]
csp1 [definition, in models.Coherence]
csp2 [definition, in models.Coherence]
cssum [definition, in models.Coherence]
cssum_coh [inductive, in models.Coherence]
cstens [definition, in models.Coherence]
cstens_compose [lemma, in models.Coherence]
cstens_id [lemma, in models.Coherence]
cstens_lmap [definition, in models.Coherence]
csterm [definition, in models.Coherence]
csunit [definition, in models.Coherence]
D
dag [definition, in models.Coherence]dag_ext_compose [lemma, in models.Coherence]
dag_counit_ext [lemma, in models.Coherence]
dag_ext_counit [lemma, in models.Coherence]
dag_ext [definition, in models.Coherence]
dag_comult_comult [lemma, in models.Coherence]
dag_comult_app_inv [lemma, in models.Coherence]
dag_comult_app [lemma, in models.Coherence]
dag_counit_comult [lemma, in models.Coherence]
dag_comult_counit [lemma, in models.Coherence]
dag_comult_natural [lemma, in models.Coherence]
dag_lmaps_app_inv [lemma, in models.Coherence]
dag_lmaps_app [lemma, in models.Coherence]
dag_comult [definition, in models.Coherence]
dag_comult_cons [constructor, in models.Coherence]
dag_comult_nil [constructor, in models.Coherence]
dag_comult_lmaps [inductive, in models.Coherence]
dag_counit_natural [lemma, in models.Coherence]
dag_counit [definition, in models.Coherence]
dag_counit_intro [constructor, in models.Coherence]
dag_counit_lmaps [inductive, in models.Coherence]
dag_compose [lemma, in models.Coherence]
dag_id [lemma, in models.Coherence]
dag_lmap [definition, in models.Coherence]
dag_lmaps_cons [constructor, in models.Coherence]
dag_lmaps_nil [constructor, in models.Coherence]
dag_lmaps [inductive, in models.Coherence]
DCPO [module, in models.DCPO]
DCPO [library]
DCPO.compose_mor [instance, in models.DCPO]
DCPO.id_mor [instance, in models.DCPO]
DCPO.Morphism [definition, in models.DCPO]
DCPO.Structure [definition, in models.DCPO]
dc_po [projection, in models.DCPO]
deq [constructor, in examples.CAL]
deq [constructor, in models.Signature]
determinism [projection, in models.IntStrat]
Deterministic [record, in models.IntStrat]
directed [definition, in models.Coherence]
directed [projection, in models.DCPO]
Directed [record, in models.DCPO]
directed [constructor, in models.DCPO]
Directed [inductive, in models.DCPO]
DirectedComplete [record, in models.DCPO]
discard [definition, in models.Coherence]
discard_uniq [lemma, in models.Coherence]
discrete [definition, in models.Signature]
dmor [definition, in models.Signature]
down [abbreviation, in lattices.Downset]
downset [abbreviation, in lattices.Downset]
Downset [module, in lattices.Downset]
Downset [library]
Downset.closed [projection, in lattices.Downset]
Downset.downset [record, in lattices.Downset]
Downset.DOWNSETS [section, in lattices.Downset]
Downset.emb [definition, in lattices.Downset]
Downset.emb_join_prime [lemma, in lattices.Downset]
Downset.emb_join_dense [lemma, in lattices.Downset]
Downset.emb_mor [lemma, in lattices.Downset]
Downset.ext [definition, in lattices.Downset]
Downset.ext_unique [lemma, in lattices.Downset]
Downset.ext_ana [lemma, in lattices.Downset]
Downset.ext_mor [instance, in lattices.Downset]
Downset.F [definition, in lattices.Downset]
Downset.Fpos [definition, in lattices.Downset]
Downset.has [projection, in lattices.Downset]
Downset.has_eq_ext [lemma, in lattices.Downset]
dsup [projection, in models.DCPO]
dsup_is_sup [projection, in models.DCPO]
D2 [module, in interfaces.Limits]
D2.compose [definition, in interfaces.Limits]
D2.compose_assoc [lemma, in interfaces.Limits]
D2.compose_id_right [lemma, in interfaces.Limits]
D2.compose_id_left [lemma, in interfaces.Limits]
D2.id [definition, in interfaces.Limits]
D2.id_def [constructor, in interfaces.Limits]
D2.m [definition, in interfaces.Limits]
D2.m_def [inductive, in interfaces.Limits]
D2.t [definition, in interfaces.Limits]
E
Ebq [inductive, in models.Signature]ecomp [definition, in models.IntStrat]
ecomp_assoc [lemma, in models.IntStrat]
ecomp_eid_r [lemma, in models.IntStrat]
ecomp_eid_l [lemma, in models.IntStrat]
econs [constructor, in models.IntStrat]
Effects [library]
EffectSignatures [library]
eid [definition, in models.IntStrat]
einl [constructor, in structures.Effects]
einr [constructor, in structures.Effects]
emor [definition, in models.IntStrat]
emor_rc_ecomp [lemma, in models.IntStrat]
emor_rc_id [lemma, in models.IntStrat]
emor_strat_intro [lemma, in models.IntStrat]
emor_strat_intro_when [lemma, in models.IntStrat]
emor_strat_elim [lemma, in models.IntStrat]
emor_strat_elim_when [lemma, in models.IntStrat]
emor_rc [definition, in models.IntStrat]
emor_rc_cont [constructor, in models.IntStrat]
emor_rc_forbid [constructor, in models.IntStrat]
emor_rc_allow [constructor, in models.IntStrat]
emor_rc_has [inductive, in models.IntStrat]
EMOR_RC [section, in models.IntStrat]
emor_strat_fcomp [lemma, in models.IntStrat]
emor_strat_fcomp_when [lemma, in models.IntStrat]
emor_strat_ecomp [lemma, in models.IntStrat]
emor_next [lemma, in models.IntStrat]
emor_next_answer [lemma, in models.IntStrat]
emor_next_question [lemma, in models.IntStrat]
emor_strat [definition, in models.IntStrat]
emor_when [definition, in models.IntStrat]
emor_answer [constructor, in models.IntStrat]
emor_suspended [constructor, in models.IntStrat]
emor_question [constructor, in models.IntStrat]
emor_ready [constructor, in models.IntStrat]
emor_has [inductive, in models.IntStrat]
EMOR_STRAT [section, in models.IntStrat]
empty_sig [inductive, in structures.Effects]
Empty_sig [definition, in models.IntStrat]
encap [definition, in models.IntStrat]
encap_prod [lemma, in models.IntStrat]
EndofunctorCategory [module, in interfaces.FunctorCategory]
EndofunctorComposition [module, in interfaces.FunctorCategory]
EndofunctorComposition.Tens [module, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.assoc [definition, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.assoc_coh [lemma, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.assoc_nat [lemma, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.lunit [definition, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.lunit_nat [lemma, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.runit [definition, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.runit_nat [lemma, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.unit [definition, in interfaces.FunctorCategory]
EndofunctorComposition.Tens.unit_coh [lemma, in interfaces.FunctorCategory]
enq [constructor, in examples.CAL]
enq [constructor, in models.Signature]
Enriched [module, in interfaces.ConcreteCategory]
Enriched.compose_mor_r [axiom, in interfaces.ConcreteCategory]
Enriched.compose_mor_l [axiom, in interfaces.ConcreteCategory]
Enriched.hom_structure [axiom, in interfaces.ConcreteCategory]
eop [projection, in models.Signature]
epos [inductive, in models.IntStrat]
Erb [inductive, in models.Signature]
eready [constructor, in models.IntStrat]
esepos [inductive, in models.IntStrat]
ese_suspended [constructor, in models.IntStrat]
ese_ready [constructor, in models.IntStrat]
esig [definition, in structures.Effects]
esig [record, in models.IntStrat]
esig_sig [definition, in models.Signature]
esig_ar [projection, in models.Signature]
esig_op [record, in models.Signature]
esipos [inductive, in models.IntStrat]
esi_suspended [constructor, in models.IntStrat]
esi_ready [constructor, in models.IntStrat]
ESTRAT_FCOMP [section, in models.IntStrat]
estrat_ecomp_when [lemma, in models.IntStrat]
ESTRAT_COMPOSE [section, in models.IntStrat]
esum [inductive, in structures.Effects]
esuspended [constructor, in models.IntStrat]
ex1 [definition, in models.Signature]
ex2 [definition, in models.Signature]
F
Faithful [module, in interfaces.Functor]FaithfulFunctor [module, in interfaces.Functor]
Faithful.faithful [axiom, in interfaces.Functor]
fassoc [definition, in models.IntStrat]
fassocr [definition, in models.IntStrat]
fassocr_fassoc [lemma, in models.IntStrat]
fassoc_iso [instance, in models.IntStrat]
fassoc_fassoc [lemma, in models.IntStrat]
fassoc_fassocr [lemma, in models.IntStrat]
fccpos [inductive, in models.IntStrat]
fccpos_suspended_r [constructor, in models.IntStrat]
fccpos_suspended_l [constructor, in models.IntStrat]
fccpos_right_r [constructor, in models.IntStrat]
fccpos_right_l [constructor, in models.IntStrat]
fccpos_left_r [constructor, in models.IntStrat]
fccpos_left_l [constructor, in models.IntStrat]
fccpos_ready [constructor, in models.IntStrat]
FCD [module, in lattices.FCD]
FCD [library]
FCDSpec [module, in lattices.FCD]
FCD.DEF [section, in lattices.FCD]
FCD.emb [definition, in lattices.FCD]
FCD.emb_mor [lemma, in lattices.FCD]
FCD.ext [definition, in lattices.FCD]
FCD.ext_unique [lemma, in lattices.FCD]
FCD.ext_ana [lemma, in lattices.FCD]
FCD.ext_mor [instance, in lattices.FCD]
FCD.F [definition, in lattices.FCD]
FCD.join_meet_dense [lemma, in lattices.FCD]
FCD.meet_join_dense [lemma, in lattices.FCD]
fcomp [definition, in models.IntStrat]
fcomp_rsq [lemma, in models.IntStrat]
fcomp_rsp [lemma, in models.IntStrat]
FCOMP_RSQ [section, in models.IntStrat]
fcomp_vcomp [lemma, in models.IntStrat]
FCOMP_VCOMP [section, in models.IntStrat]
fcomp_vid [lemma, in models.IntStrat]
FCOMP_VID [section, in models.IntStrat]
fcomp_inf_r [lemma, in models.IntStrat]
fcomp_inf_l [lemma, in models.IntStrat]
fcomp_sup_r [lemma, in models.IntStrat]
fcomp_sup_l [lemma, in models.IntStrat]
fcomp_rc [definition, in models.IntStrat]
fcomp_rc_has [definition, in models.IntStrat]
FCOMP_RC [section, in models.IntStrat]
fcomp_compose [lemma, in models.IntStrat]
fcomp_compose_when [lemma, in models.IntStrat]
fcomp_compose_has [lemma, in models.IntStrat]
fcomp_id [lemma, in models.IntStrat]
fcomp_st [abbreviation, in models.IntStrat]
fcomp_next_pa_r [lemma, in models.IntStrat]
fcomp_next_pa_l [lemma, in models.IntStrat]
fcomp_next_oa_r [lemma, in models.IntStrat]
fcomp_next_oa_l [lemma, in models.IntStrat]
fcomp_next_pq_r [lemma, in models.IntStrat]
fcomp_next_pq_l [lemma, in models.IntStrat]
fcomp_next_oq_r [lemma, in models.IntStrat]
fcomp_next_oq_l [lemma, in models.IntStrat]
fcomp_when [definition, in models.IntStrat]
fcomp_has_closed [lemma, in models.IntStrat]
fcomp_pa_r [constructor, in models.IntStrat]
fcomp_pa_l [constructor, in models.IntStrat]
fcomp_oa_r [constructor, in models.IntStrat]
fcomp_oa_l [constructor, in models.IntStrat]
fcomp_suspended_r [constructor, in models.IntStrat]
fcomp_suspended_l [constructor, in models.IntStrat]
fcomp_pq_r [constructor, in models.IntStrat]
fcomp_pq_l [constructor, in models.IntStrat]
fcomp_oq_r [constructor, in models.IntStrat]
fcomp_oq_l [constructor, in models.IntStrat]
fcomp_ready [constructor, in models.IntStrat]
fcomp_has [inductive, in models.IntStrat]
FCOMP_STRAT [section, in models.IntStrat]
fcomp_ecomp [lemma, in models.IntStrat]
fcomp_eid [lemma, in models.IntStrat]
fcomp_emor [definition, in models.IntStrat]
fcpos [inductive, in models.IntStrat]
fcpos_suspended_r [constructor, in models.IntStrat]
fcpos_suspended_l [constructor, in models.IntStrat]
fcpos_running_r [constructor, in models.IntStrat]
fcpos_running_l [constructor, in models.IntStrat]
fcpos_ready [constructor, in models.IntStrat]
fcrspos [inductive, in models.IntStrat]
fcrs_suspended_r [constructor, in models.IntStrat]
fcrs_suspended_l [constructor, in models.IntStrat]
fcrs_running_r [constructor, in models.IntStrat]
fcrs_running_l [constructor, in models.IntStrat]
fcrs_ready [constructor, in models.IntStrat]
fdrop [definition, in models.IntStrat]
fdrop_uniq [lemma, in models.IntStrat]
fdup [definition, in models.IntStrat]
ffst [definition, in models.IntStrat]
ffst_fdelta [instance, in models.IntStrat]
ffst_fdup [lemma, in models.IntStrat]
ffst_fdrop [lemma, in models.IntStrat]
finf [definition, in structures.Lattice]
finf_glb [lemma, in structures.Lattice]
finf_at [lemma, in structures.Lattice]
finf_lb [lemma, in structures.Lattice]
flu [definition, in models.IntStrat]
flur [definition, in models.IntStrat]
flur_flu [lemma, in models.IntStrat]
flu_iso [instance, in models.IntStrat]
flu_fassoc [lemma, in models.IntStrat]
flu_flur [lemma, in models.IntStrat]
fpair [definition, in models.IntStrat]
FPAIR [section, in models.IntStrat]
fpair_expand [lemma, in models.IntStrat]
fpair_uniq [lemma, in models.IntStrat]
free_m [definition, in models.Sets]
free_f [definition, in models.Sets]
fru [definition, in models.IntStrat]
frur [definition, in models.IntStrat]
frur_fru [lemma, in models.IntStrat]
fru_iso [instance, in models.IntStrat]
fru_frur [lemma, in models.IntStrat]
fsnd [definition, in models.IntStrat]
fsnd_fdelta [instance, in models.IntStrat]
fsnd_fdup [lemma, in models.IntStrat]
fsnd_fdrop [lemma, in models.IntStrat]
fsup [definition, in structures.Lattice]
fsup_lub [lemma, in structures.Lattice]
fsup_at [lemma, in structures.Lattice]
fsup_ub [lemma, in structures.Lattice]
fswap [definition, in models.IntStrat]
fswap_iso [instance, in models.IntStrat]
fswap_fswap [lemma, in models.IntStrat]
fswap_assoc [lemma, in models.IntStrat]
fswap_unit [lemma, in models.IntStrat]
Full [module, in interfaces.Functor]
FullAndFaithfulFunctor [module, in interfaces.Functor]
FullFunctor [module, in interfaces.Functor]
Full.full [axiom, in interfaces.Functor]
Functor [module, in interfaces.Functor]
Functor [library]
FunctorCategory [module, in interfaces.FunctorCategory]
FunctorCategory [library]
FunctorCategoryInstance [module, in interfaces.FunctorCategory]
FunctorCategory.comp [projection, in interfaces.FunctorCategory]
FunctorCategory.compose [definition, in interfaces.FunctorCategory]
FunctorCategory.compose_assoc [lemma, in interfaces.FunctorCategory]
FunctorCategory.compose_id_right [lemma, in interfaces.FunctorCategory]
FunctorCategory.compose_id_left [lemma, in interfaces.FunctorCategory]
FunctorCategory.fapply [projection, in interfaces.FunctorCategory]
FunctorCategory.fapply_compose [projection, in interfaces.FunctorCategory]
FunctorCategory.fapply_id [projection, in interfaces.FunctorCategory]
FunctorCategory.functor [record, in interfaces.FunctorCategory]
FunctorCategory.id [definition, in interfaces.FunctorCategory]
FunctorCategory.m [definition, in interfaces.FunctorCategory]
FunctorCategory.meq [lemma, in interfaces.FunctorCategory]
FunctorCategory.mknt [constructor, in interfaces.FunctorCategory]
FunctorCategory.natural [projection, in interfaces.FunctorCategory]
FunctorCategory.natural_rewrite [lemma, in interfaces.FunctorCategory]
FunctorCategory.nt [record, in interfaces.FunctorCategory]
FunctorCategory.oapply [projection, in interfaces.FunctorCategory]
FunctorCategory.t [definition, in interfaces.FunctorCategory]
FunctorComposition [module, in interfaces.FunctorCategory]
FunctorComposition.fmap [definition, in interfaces.FunctorCategory]
FunctorComposition.fmap_compose [lemma, in interfaces.FunctorCategory]
FunctorComposition.fmap_id [lemma, in interfaces.FunctorCategory]
FunctorComposition.omap [definition, in interfaces.FunctorCategory]
FunctorDefinition [module, in interfaces.Functor]
FunctorDefinition.fmap [axiom, in interfaces.Functor]
FunctorDefinition.fmap_compose [axiom, in interfaces.Functor]
FunctorDefinition.fmap_id [axiom, in interfaces.Functor]
FunctorDefinition.omap [axiom, in interfaces.Functor]
FunctorMonoidal [module, in interfaces.MonoidalCategory]
FunctorMonoidal.omap_prod_nat [axiom, in interfaces.MonoidalCategory]
FunctorMonoidal.omap_prod [axiom, in interfaces.MonoidalCategory]
FunctorMonoidal.omap_unit [axiom, in interfaces.MonoidalCategory]
FunctorTheory [module, in interfaces.Functor]
FunctorTheory.fmap_iso [definition, in interfaces.Functor]
funext_rel [instance, in models.IntStrat]
funext_subrel [instance, in models.IntStrat]
fw [projection, in models.IntStrat]
fw_bw [projection, in models.IntStrat]
G
get [constructor, in examples.CAL]get [constructor, in models.Signature]
get [projection, in models.IntStrat]
getbit [constructor, in models.Sets]
get_eqv [projection, in models.IntStrat]
get_set [projection, in models.IntStrat]
glob [definition, in models.IntStrat]
H
has [projection, in models.Coherence]has_coh [projection, in models.Coherence]
hmap [definition, in models.Signature]
hmap_compose [lemma, in models.Signature]
hmap_id [lemma, in models.Signature]
hmap_basis [lemma, in models.Signature]
hmap_natural [lemma, in models.Signature]
I
id [projection, in structures.Category]id [abbreviation, in models.IntStrat]
id_compose [projection, in structures.Category]
ID_RSQ [section, in models.IntStrat]
id_cpos_r [definition, in models.IntStrat]
id_idpos_r [definition, in models.IntStrat]
id_pos_r [definition, in models.IntStrat]
id_cpos_l [definition, in models.IntStrat]
id_idpos_l [definition, in models.IntStrat]
id_pos_l [definition, in models.IntStrat]
id_next [lemma, in models.IntStrat]
im [inductive, in models.DCPO]
imap [definition, in models.Coherence]
imap_compose [lemma, in models.Coherence]
imap_id [lemma, in models.Coherence]
im_directed [instance, in models.DCPO]
im_compose [lemma, in models.DCPO]
im_id [lemma, in models.DCPO]
im_intro [constructor, in models.DCPO]
inc1 [constructor, in examples.CAL]
inc1 [constructor, in models.Signature]
inc2 [constructor, in examples.CAL]
inc2 [constructor, in models.Signature]
Inf [module, in lattices.Upset]
inf_sup [lemma, in structures.Lattice]
inf_iff [lemma, in structures.Lattice]
inf_at [lemma, in structures.Lattice]
inf_glb [projection, in structures.Lattice]
inf_lb [projection, in structures.Lattice]
inf_eq [instance, in models.IntStrat]
Inf.compose_mor [lemma, in lattices.Upset]
Inf.id_mor [lemma, in lattices.Upset]
Inf.mor [projection, in lattices.Upset]
Inf.mor [constructor, in lattices.Upset]
Inf.Morphism [record, in lattices.Upset]
Inf.Morphism [inductive, in lattices.Upset]
Inf.mor_ref [lemma, in lattices.Upset]
Inf.mor_meet [lemma, in lattices.Upset]
init_state_eqv [projection, in models.IntStrat]
init_state [projection, in models.IntStrat]
inl_inr_coh [constructor, in models.Coherence]
inl_coh [constructor, in models.Coherence]
input [definition, in models.Coherence]
inr_inl_coh [constructor, in models.Coherence]
inr_coh [constructor, in models.Coherence]
interp [record, in structures.Effects]
InterpMorphism [record, in structures.Effects]
intm_lmor [projection, in structures.Effects]
IntSpec [library]
IntStrat [library]
inv [definition, in models.IntStrat]
inv_pswap [lemma, in models.IntStrat]
inv_r [lemma, in models.IntStrat]
inv_l [lemma, in models.IntStrat]
inv_invol [lemma, in models.IntStrat]
Isomorphism [record, in models.IntStrat]
iso_bw [projection, in models.IntStrat]
iso_fw [projection, in models.IntStrat]
ispec [abbreviation, in models.IntSpec]
ISpec [module, in models.IntSpec]
ISpec.apply [definition, in models.IntSpec]
ISpec.apply_assoc [lemma, in models.IntSpec]
ISpec.apply_int_l [lemma, in models.IntSpec]
ISpec.apply_int_r [lemma, in models.IntSpec]
ISpec.apply_bind [lemma, in models.IntSpec]
ISpec.apply_ret [lemma, in models.IntSpec]
ISpec.apply_mor_params [instance, in models.IntSpec]
ISpec.apply_mor [instance, in models.IntSpec]
ISpec.bind [definition, in models.IntSpec]
ISpec.bind_bind [lemma, in models.IntSpec]
ISpec.bind_ret_l [lemma, in models.IntSpec]
ISpec.bind_ret_r [lemma, in models.IntSpec]
ISpec.bind_mor_params [instance, in models.IntSpec]
ISpec.bind_mor [instance, in models.IntSpec]
ISpec.compose [definition, in models.IntSpec]
ISpec.compose_assoc [lemma, in models.IntSpec]
ISpec.compose_int_r [lemma, in models.IntSpec]
ISpec.compose_int_l [lemma, in models.IntSpec]
ISpec.int [definition, in models.IntSpec]
ISpec.papply [definition, in models.IntSpec]
ISpec.papply_mor [instance, in models.IntSpec]
ISpec.pbind [definition, in models.IntSpec]
ISpec.pbind_ret_l [lemma, in models.IntSpec]
ISpec.pbind_mor [instance, in models.IntSpec]
ISpec.pcons [constructor, in models.IntSpec]
ISpec.pcons_ref [constructor, in models.IntSpec]
ISpec.play [inductive, in models.IntSpec]
ISpec.play_poset [definition, in models.IntSpec]
ISpec.pmove [constructor, in models.IntSpec]
ISpec.pmove_cons_ref [constructor, in models.IntSpec]
ISpec.pmove_ref [constructor, in models.IntSpec]
ISpec.pref [inductive, in models.IntSpec]
ISpec.pref_antisym [instance, in models.IntSpec]
ISpec.pref_preo [instance, in models.IntSpec]
ISpec.pret [constructor, in models.IntSpec]
ISpec.pret_ref [constructor, in models.IntSpec]
ISpec.ret [definition, in models.IntSpec]
ISpec.subst [definition, in models.IntSpec]
ISpec.t [definition, in models.IntSpec]
IsSup [record, in models.DCPO]
J
join [definition, in structures.Lattice]JoinMeetDense [module, in lattices.FCD]
JoinMeetDense.join_meet_dense [axiom, in lattices.FCD]
JoinMeetDense.meet_join_dense [axiom, in lattices.FCD]
join_idemp [lemma, in structures.Lattice]
join_comm [lemma, in structures.Lattice]
join_meet_l [lemma, in structures.Lattice]
join_top_l [lemma, in structures.Lattice]
join_bot_l [lemma, in structures.Lattice]
join_r [lemma, in structures.Lattice]
join_l [lemma, in structures.Lattice]
join_lub [lemma, in structures.Lattice]
join_ub_r [lemma, in structures.Lattice]
join_ub_l [lemma, in structures.Lattice]
L
Lattice [library]LatticeCategory [module, in structures.Completion]
LatticeCategory.compose_mor [axiom, in structures.Completion]
LatticeCategory.id_mor [axiom, in structures.Completion]
LatticeCategory.Morphism [axiom, in structures.Completion]
LatticeCategory.mor_ref [axiom, in structures.Completion]
LatticeCompletion [module, in structures.Completion]
LatticeCompletionDefs [module, in structures.Completion]
LatticeCompletionDefs.emb_params [instance, in structures.Completion]
LatticeCompletionDefs.emb_mor' [instance, in structures.Completion]
LatticeCompletionDefs.ext_params [instance, in structures.Completion]
LatticeCompletionDefs.ext_ext [lemma, in structures.Completion]
LatticeCompletionDefs.ext_emb [lemma, in structures.Completion]
LatticeCompletionDefs.map [definition, in structures.Completion]
LatticeCompletionDefs.map_params [instance, in structures.Completion]
LatticeCompletionDefs.map_mor [instance, in structures.Completion]
LatticeCompletionSpec [module, in structures.Completion]
LatticeCompletionSpec.DEFS [section, in structures.Completion]
LatticeCompletionSpec.emb [axiom, in structures.Completion]
LatticeCompletionSpec.emb_mor [axiom, in structures.Completion]
LatticeCompletionSpec.ext [axiom, in structures.Completion]
LatticeCompletionSpec.ext_unique [axiom, in structures.Completion]
LatticeCompletionSpec.ext_ana [axiom, in structures.Completion]
LatticeCompletionSpec.ext_mor [axiom, in structures.Completion]
LatticeCompletionSpec.F [axiom, in structures.Completion]
LatticeProduct [library]
layer [definition, in examples.CAL]
Lazy [module, in lattices.AdjoinBot]
LazyMorphism [record, in structures.Effects]
Lazy.cmor_inf [instance, in lattices.AdjoinBot]
Lazy.cmor_sup [instance, in lattices.AdjoinBot]
Lazy.compose_mor [lemma, in lattices.AdjoinBot]
Lazy.DEF [section, in lattices.AdjoinBot]
Lazy.id_mor [lemma, in lattices.AdjoinBot]
Lazy.mor [projection, in lattices.AdjoinBot]
Lazy.mor [constructor, in lattices.AdjoinBot]
Lazy.Morphism [record, in lattices.AdjoinBot]
Lazy.Morphism [inductive, in lattices.AdjoinBot]
Lazy.mor_ref [instance, in lattices.AdjoinBot]
Lazy.mor_sup [projection, in lattices.AdjoinBot]
Lazy.mor_sup [constructor, in lattices.AdjoinBot]
Lazy.NSupMorphism [record, in lattices.AdjoinBot]
Lazy.NSupMorphism [inductive, in lattices.AdjoinBot]
LBot [module, in lattices.AdjoinBot]
LBot.cases [lemma, in lattices.AdjoinBot]
LBot.DEF [section, in lattices.AdjoinBot]
LBot.emb [definition, in lattices.AdjoinBot]
LBot.emb_mor [instance, in lattices.AdjoinBot]
LBot.ext [definition, in lattices.AdjoinBot]
LBot.ext_unique [lemma, in lattices.AdjoinBot]
LBot.ext_mor [instance, in lattices.AdjoinBot]
LBot.ext_ana [lemma, in lattices.AdjoinBot]
LBot.ext_bot [lemma, in lattices.AdjoinBot]
LBot.F [definition, in lattices.AdjoinBot]
LBot.Fposet [definition, in lattices.AdjoinBot]
LBot.inf_sup_of [definition, in lattices.AdjoinBot]
LBot.inf_of [definition, in lattices.AdjoinBot]
LBot.is [definition, in lattices.AdjoinBot]
LBot.is_unique [lemma, in lattices.AdjoinBot]
LBot.mkopt [constructor, in lattices.AdjoinBot]
LBot.opt [inductive, in lattices.AdjoinBot]
LBot.opt_eq [lemma, in lattices.AdjoinBot]
LBot.proj [definition, in lattices.AdjoinBot]
LBot.proj_is [lemma, in lattices.AdjoinBot]
LBot.sup_cases [lemma, in lattices.AdjoinBot]
LBot.sup_inf_of_cd [lemma, in lattices.AdjoinBot]
LBot.sup_inf_of [definition, in lattices.AdjoinBot]
LBot.sup_of [definition, in lattices.AdjoinBot]
lcdlm_sup [projection, in structures.Effects]
lcdlm_inf [projection, in structures.Effects]
lcj [definition, in models.IntStrat]
lcjepos [inductive, in models.IntStrat]
lcje_suspended [constructor, in models.IntStrat]
lcje_running [constructor, in models.IntStrat]
lcje_ready [constructor, in models.IntStrat]
lcjipos [inductive, in models.IntStrat]
lcji_suspended [constructor, in models.IntStrat]
lcji_running [constructor, in models.IntStrat]
lcji_ready [constructor, in models.IntStrat]
lcj_elim [lemma, in models.IntStrat]
lcj_elim_when [lemma, in models.IntStrat]
lcj_intro [lemma, in models.IntStrat]
lcj_intro_when [lemma, in models.IntStrat]
lcj_when [definition, in models.IntStrat]
lcj_has [definition, in models.IntStrat]
lcomp [definition, in models.IntStrat]
lcomp_lcomp [lemma, in models.IntStrat]
lcomp_lid_r [lemma, in models.IntStrat]
lcomp_lid_l [lemma, in models.IntStrat]
lconv [definition, in models.IntStrat]
lcp [definition, in models.IntStrat]
lcpepos [inductive, in models.IntStrat]
lcpe_suspended [constructor, in models.IntStrat]
lcpe_running [constructor, in models.IntStrat]
lcpe_ready [constructor, in models.IntStrat]
lcpipos [inductive, in models.IntStrat]
lcpi_suspended [constructor, in models.IntStrat]
lcpi_running [constructor, in models.IntStrat]
lcpi_ready [constructor, in models.IntStrat]
lcp_elim [lemma, in models.IntStrat]
lcp_elim_when [lemma, in models.IntStrat]
lcp_intro [lemma, in models.IntStrat]
lcp_intro_when [lemma, in models.IntStrat]
lcp_when [definition, in models.IntStrat]
lcp_has [definition, in models.IntStrat]
ldrop [definition, in models.IntStrat]
le [projection, in models.DCPO]
lens [record, in models.IntStrat]
LENS_RC [section, in models.IntStrat]
lens_strat_eq [instance, in models.IntStrat]
lens_strat_ref [lemma, in models.IntStrat]
LENS_STRAT_REF [section, in models.IntStrat]
lens_strat_next_pa [lemma, in models.IntStrat]
lens_strat_next_oa [lemma, in models.IntStrat]
lens_strat_next_pq [lemma, in models.IntStrat]
lens_strat_next_oq [lemma, in models.IntStrat]
lens_strat [definition, in models.IntStrat]
lens_strat_when [definition, in models.IntStrat]
lens_pa [constructor, in models.IntStrat]
lens_oa [constructor, in models.IntStrat]
lens_suspended [constructor, in models.IntStrat]
lens_pq [constructor, in models.IntStrat]
lens_oq [constructor, in models.IntStrat]
lens_ready [constructor, in models.IntStrat]
lens_has [inductive, in models.IntStrat]
LENS_STRAT [section, in models.IntStrat]
lens_eqv [record, in models.IntStrat]
le_directed [lemma, in models.DCPO]
le_po [projection, in models.DCPO]
le_preo [projection, in models.DCPO]
lid [abbreviation, in models.IntStrat]
lim [definition, in models.Coherence]
Limits [module, in interfaces.Limits]
Limits [library]
LimitsPreliminaries [module, in interfaces.Limits]
LimitsPreliminaries.cone [record, in interfaces.Limits]
LimitsPreliminaries.cone_mor_eq [lemma, in interfaces.Limits]
LimitsPreliminaries.cone_mor [record, in interfaces.Limits]
LimitsPreliminaries.Diagram [module, in interfaces.Limits]
LimitsPreliminaries.edge [projection, in interfaces.Limits]
LimitsPreliminaries.edge_mor [projection, in interfaces.Limits]
LimitsPreliminaries.face [projection, in interfaces.Limits]
LimitsPreliminaries.Limit [record, in interfaces.Limits]
LimitsPreliminaries.lim_uni [projection, in interfaces.Limits]
LimitsPreliminaries.lim_mor [projection, in interfaces.Limits]
LimitsPreliminaries.vertex [projection, in interfaces.Limits]
LimitsPreliminaries.vertex_mor [projection, in interfaces.Limits]
Limits.lim [axiom, in interfaces.Limits]
Limits.lim_spec [axiom, in interfaces.Limits]
lim_sup [lemma, in models.Coherence]
LinCCAL [module, in models.LinCCAL]
LinCCAL [library]
LinCCALBase [module, in models.LinCCAL]
LinCCALBase.cal [definition, in models.LinCCAL]
LinCCALBase.ci_next [projection, in models.LinCCAL]
LinCCALBase.ci_safe [projection, in models.LinCCAL]
LinCCALBase.ci_valid [projection, in models.LinCCAL]
LinCCALBase.compose [definition, in models.LinCCAL]
LinCCALBase.COMPOSE [section, in models.LinCCAL]
LinCCALBase.compose_assoc [lemma, in models.LinCCAL]
LinCCALBase.compose_id_right [lemma, in models.LinCCAL]
LinCCALBase.compose_id_left [lemma, in models.LinCCAL]
LinCCALBase.comp_cal [lemma, in models.LinCCAL]
LinCCALBase.comp_ci [lemma, in models.LinCCAL]
LinCCALBase.comp_run [lemma, in models.LinCCAL]
LinCCALBase.comp_run_r [lemma, in models.LinCCAL]
LinCCALBase.comp_specified_sufficient [lemma, in models.LinCCAL]
LinCCALBase.comp_state [definition, in models.LinCCAL]
LinCCALBase.comp_state_intro [constructor, in models.LinCCAL]
LinCCALBase.comp_state_def [inductive, in models.LinCCAL]
LinCCALBase.comp_tmap_commit_r [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_commit_l [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_return_r [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_action_r [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_invoke_r [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_return_l [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_action_l [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_invoke_l [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_specified_r [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_specified_l [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap_convert [lemma, in models.LinCCAL]
LinCCALBase.comp_tmap [definition, in models.LinCCAL]
LinCCALBase.comp_threadstate_o [lemma, in models.LinCCAL]
LinCCALBase.comp_threadstate_valid [lemma, in models.LinCCAL]
LinCCALBase.comp_threadstate [inductive, in models.LinCCAL]
LinCCALBase.comp_running [constructor, in models.LinCCAL]
LinCCALBase.comp_ready [constructor, in models.LinCCAL]
LinCCALBase.comp_phase [inductive, in models.LinCCAL]
LinCCALBase.correct [record, in models.LinCCAL]
LinCCALBase.correctness_invariant_sound [lemma, in models.LinCCAL]
LinCCALBase.correctness_invariant [record, in models.LinCCAL]
LinCCALBase.correct_ci [lemma, in models.LinCCAL]
LinCCALBase.correct_next [projection, in models.LinCCAL]
LinCCALBase.correct_safe [projection, in models.LinCCAL]
LinCCALBase.correct_valid [projection, in models.LinCCAL]
LinCCALBase.cts_right [constructor, in models.LinCCAL]
LinCCALBase.cts_left [constructor, in models.LinCCAL]
LinCCALBase.cts_ready [constructor, in models.LinCCAL]
LinCCALBase.eaction [constructor, in models.LinCCAL]
LinCCALBase.einvoke [constructor, in models.LinCCAL]
LinCCALBase.ereturn [constructor, in models.LinCCAL]
LinCCALBase.estep [inductive, in models.LinCCAL]
LinCCALBase.id [definition, in models.LinCCAL]
LinCCALBase.id_cal [lemma, in models.LinCCAL]
LinCCALBase.id_state_ci [lemma, in models.LinCCAL]
LinCCALBase.id_state_intro [constructor, in models.LinCCAL]
LinCCALBase.id_state [inductive, in models.LinCCAL]
LinCCALBase.id_returned [constructor, in models.LinCCAL]
LinCCALBase.id_invoked [constructor, in models.LinCCAL]
LinCCALBase.id_linstate [inductive, in models.LinCCAL]
LinCCALBase.layer_implementation [record, in models.LinCCAL]
LinCCALBase.layer_interface [record, in models.LinCCAL]
LinCCALBase.lcommit [constructor, in models.LinCCAL]
LinCCALBase.li_correct [projection, in models.LinCCAL]
LinCCALBase.li_impl [projection, in models.LinCCAL]
LinCCALBase.li_spec [projection, in models.LinCCAL]
LinCCALBase.li_sig [projection, in models.LinCCAL]
LinCCALBase.lstep [inductive, in models.LinCCAL]
LinCCALBase.lsteps_ind [lemma, in models.LinCCAL]
LinCCALBase.m [definition, in models.LinCCAL]
LinCCALBase.meq [lemma, in models.LinCCAL]
LinCCALBase.mkst [constructor, in models.LinCCAL]
LinCCALBase.mkts [constructor, in models.LinCCAL]
LinCCALBase.pending_program [definition, in models.LinCCAL]
LinCCALBase.reachable [definition, in models.LinCCAL]
LinCCALBase.reachable_steps [lemma, in models.LinCCAL]
LinCCALBase.reachable_step [lemma, in models.LinCCAL]
LinCCALBase.reachable_base [lemma, in models.LinCCAL]
LinCCALBase.run_check_r_var [constructor, in models.LinCCAL]
LinCCALBase.run_check_r_cons [constructor, in models.LinCCAL]
LinCCALBase.run_check_r [inductive, in models.LinCCAL]
LinCCALBase.run_check_l_var [constructor, in models.LinCCAL]
LinCCALBase.run_check_l_cons [constructor, in models.LinCCAL]
LinCCALBase.run_check_l [inductive, in models.LinCCAL]
LinCCALBase.spec [abbreviation, in models.LinCCAL]
LinCCALBase.Spec [module, in models.LinCCAL]
LinCCALBase.specified [definition, in models.LinCCAL]
LinCCALBase.Spec.bot [constructor, in models.LinCCAL]
LinCCALBase.Spec.gen [definition, in models.LinCCAL]
LinCCALBase.Spec.lts [abbreviation, in models.LinCCAL]
LinCCALBase.Spec.next [projection, in models.LinCCAL]
LinCCALBase.Spec.outcome [inductive, in models.LinCCAL]
LinCCALBase.Spec.ret [constructor, in models.LinCCAL]
LinCCALBase.Spec.t [record, in models.LinCCAL]
LinCCALBase.Spec.tens [definition, in models.LinCCAL]
LinCCALBase.Spec.tens_lts [definition, in models.LinCCAL]
LinCCALBase.Spec.top [constructor, in models.LinCCAL]
LinCCALBase.star [abbreviation, in models.LinCCAL]
LinCCALBase.state [record, in models.LinCCAL]
LinCCALBase.st_base [projection, in models.LinCCAL]
LinCCALBase.st_impl [projection, in models.LinCCAL]
LinCCALBase.st_spec [projection, in models.LinCCAL]
LinCCALBase.t [definition, in models.LinCCAL]
LinCCALBase.threadstate [record, in models.LinCCAL]
LinCCALBase.threadstate_valid [definition, in models.LinCCAL]
LinCCALBase.tid [abbreviation, in models.LinCCAL]
LinCCALBase.tmap [abbreviation, in models.LinCCAL]
LinCCALBase.TMap [module, in models.LinCCAL]
LinCCALBase.ts_res [projection, in models.LinCCAL]
LinCCALBase.ts_prog [projection, in models.LinCCAL]
LinCCALBase.ts_op [projection, in models.LinCCAL]
_ * _ (spec_scope) [notation, in models.LinCCAL]
_ <- _ ; _ [notation, in models.LinCCAL]
_ >>= _ [notation, in models.LinCCAL]
LinCCALExample [module, in models.LinCCAL]
LinCCALExample.acq [constructor, in models.LinCCAL]
LinCCALExample.Ecounter [definition, in models.LinCCAL]
LinCCALExample.Ecounter_op [inductive, in models.LinCCAL]
LinCCALExample.Elock [definition, in models.LinCCAL]
LinCCALExample.Elock_op [inductive, in models.LinCCAL]
LinCCALExample.Ereg [definition, in models.LinCCAL]
LinCCALExample.Ereg_ar [definition, in models.LinCCAL]
LinCCALExample.Ereg_op [inductive, in models.LinCCAL]
LinCCALExample.fai [constructor, in models.LinCCAL]
LinCCALExample.fai_threadstate_convert [lemma, in models.LinCCAL]
LinCCALExample.fai_state_intro [constructor, in models.LinCCAL]
LinCCALExample.fai_state [inductive, in models.LinCCAL]
LinCCALExample.fai_ret [constructor, in models.LinCCAL]
LinCCALExample.fai_rel [constructor, in models.LinCCAL]
LinCCALExample.fai_set [constructor, in models.LinCCAL]
LinCCALExample.fai_get [constructor, in models.LinCCAL]
LinCCALExample.fai_acq [constructor, in models.LinCCAL]
LinCCALExample.fai_rdy [constructor, in models.LinCCAL]
LinCCALExample.fai_threadstate [inductive, in models.LinCCAL]
LinCCALExample.fai_impl [definition, in models.LinCCAL]
LinCCALExample.get [constructor, in models.LinCCAL]
LinCCALExample.Lcounter [definition, in models.LinCCAL]
LinCCALExample.Llock [definition, in models.LinCCAL]
LinCCALExample.Lreg [definition, in models.LinCCAL]
LinCCALExample.Mcounter [definition, in models.LinCCAL]
LinCCALExample.rel [constructor, in models.LinCCAL]
LinCCALExample.set [constructor, in models.LinCCAL]
LinCCALExample.Σcounter [definition, in models.LinCCAL]
LinCCALExample.Σlock [definition, in models.LinCCAL]
LinCCALExample.Σreg [definition, in models.LinCCAL]
LinCCALTens [module, in models.LinCCAL]
LinCCALTensSpec [module, in models.LinCCAL]
LinCCALTens.Tens [module, in models.LinCCAL]
LinCCALTens.Tens.assoc [definition, in models.LinCCAL]
LinCCALTens.Tens.assoc_coh [lemma, in models.LinCCAL]
LinCCALTens.Tens.assoc_nat [lemma, in models.LinCCAL]
LinCCALTens.Tens.assoc_bw_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.assoc_bw_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.assoc_fw_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.assoc_fw_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.CORRECTNESS [section, in models.LinCCAL]
LinCCALTens.Tens.fmap [definition, in models.LinCCAL]
LinCCALTens.Tens.fmap_compose [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_id [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_ci [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_lsteps_r [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_lsteps_l [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.fmap_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.fmap_tmap_specified_r [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_tmap_specified_l [lemma, in models.LinCCAL]
LinCCALTens.Tens.fmap_tmap [definition, in models.LinCCAL]
LinCCALTens.Tens.fmap_ts_right [constructor, in models.LinCCAL]
LinCCALTens.Tens.fmap_ts_left [constructor, in models.LinCCAL]
LinCCALTens.Tens.fmap_ts_none [constructor, in models.LinCCAL]
LinCCALTens.Tens.fmap_threadstate [inductive, in models.LinCCAL]
LinCCALTens.Tens.inj_somets2 [lemma, in models.LinCCAL]
LinCCALTens.Tens.iso_tmap [definition, in models.LinCCAL]
LinCCALTens.Tens.iso_returned [constructor, in models.LinCCAL]
LinCCALTens.Tens.iso_invoked [constructor, in models.LinCCAL]
LinCCALTens.Tens.iso_threadstate [inductive, in models.LinCCAL]
LinCCALTens.Tens.ISO_CORRECTNESS [section, in models.LinCCAL]
LinCCALTens.Tens.lunit [definition, in models.LinCCAL]
LinCCALTens.Tens.lunit_nat [lemma, in models.LinCCAL]
LinCCALTens.Tens.lunit_bw_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.lunit_bw_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.lunit_fw_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.lunit_fw_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.omap [definition, in models.LinCCAL]
LinCCALTens.Tens.runit [definition, in models.LinCCAL]
LinCCALTens.Tens.runit_swap [lemma, in models.LinCCAL]
LinCCALTens.Tens.runit_nat [lemma, in models.LinCCAL]
LinCCALTens.Tens.runit_bw_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.runit_bw_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.runit_fw_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.runit_fw_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.swap [definition, in models.LinCCAL]
LinCCALTens.Tens.swap_swap [lemma, in models.LinCCAL]
LinCCALTens.Tens.swap_assoc [lemma, in models.LinCCAL]
LinCCALTens.Tens.swap_nat [lemma, in models.LinCCAL]
LinCCALTens.Tens.swap_state_intro [constructor, in models.LinCCAL]
LinCCALTens.Tens.swap_state [inductive, in models.LinCCAL]
LinCCALTens.Tens.unit [definition, in models.LinCCAL]
LinCCALTens.Tens.unit_coh [lemma, in models.LinCCAL]
_ * _ (hom_scope) [notation, in models.LinCCAL]
_ * _ (obj_scope) [notation, in models.LinCCAL]
_ + _ [notation, in models.LinCCAL]
linf [projection, in structures.Lattice]
list_coh [inductive, in models.Coherence]
lmap [definition, in models.Coherence]
lmap_flip [definition, in models.Coherence]
lmap_apply_compose [lemma, in models.Coherence]
lmap_apply_id [lemma, in models.Coherence]
lmap_apply [definition, in models.Coherence]
lmap_compose_assoc [lemma, in models.Coherence]
lmap_compose_id_right [lemma, in models.Coherence]
lmap_compose_id_left [lemma, in models.Coherence]
lmap_compose [definition, in models.Coherence]
lmap_id [definition, in models.Coherence]
lmap_ext [lemma, in models.Coherence]
lmap_det [lemma, in models.Coherence]
lmap_coh [lemma, in models.Coherence]
ln [constructor, in models.Coherence]
lneg [definition, in models.Coherence]
lneg_coh_intro [constructor, in models.Coherence]
lneg_coh [inductive, in models.Coherence]
lneg_token [inductive, in models.Coherence]
lpos [inductive, in models.IntStrat]
lpos_eqv [inductive, in models.IntStrat]
lready [constructor, in models.IntStrat]
lready_eqv [constructor, in models.IntStrat]
lrunning [constructor, in models.IntStrat]
lrunning_eqv [constructor, in models.IntStrat]
lsq [definition, in models.IntStrat]
lsup [projection, in structures.Lattice]
lsuspended [constructor, in models.IntStrat]
lsuspended_eqv [constructor, in models.IntStrat]
L_rb [definition, in examples.CAL]
L_bq [definition, in examples.CAL]
M
meet [definition, in structures.Lattice]meet_idemp [lemma, in structures.Lattice]
meet_comm [lemma, in structures.Lattice]
meet_r [lemma, in structures.Lattice]
meet_l [lemma, in structures.Lattice]
meet_glb [lemma, in structures.Lattice]
meet_lb_r [lemma, in structures.Lattice]
meet_lb_l [lemma, in structures.Lattice]
Monad [library]
Monads [module, in interfaces.FunctorCategory]
Monoidal [module, in interfaces.MonoidalCategory]
MonoidalCategory [module, in interfaces.MonoidalCategory]
MonoidalCategory [module, in interfaces.FunctorCategory]
MonoidalCategory [library]
MonoidalClosureDefinition [module, in interfaces.MonoidalCategory]
MonoidalClosureDefinition.curry [axiom, in interfaces.MonoidalCategory]
MonoidalClosureDefinition.curry_natural_r [axiom, in interfaces.MonoidalCategory]
MonoidalClosureDefinition.curry_natural_l [axiom, in interfaces.MonoidalCategory]
MonoidalClosureDefinition.curry_uncurry [axiom, in interfaces.MonoidalCategory]
MonoidalClosureDefinition.uncurry [axiom, in interfaces.MonoidalCategory]
MonoidalClosureDefinition.uncurry_curry [axiom, in interfaces.MonoidalCategory]
_ * _ (hom_scope) [notation, in interfaces.MonoidalCategory]
_ * _ (obj_scope) [notation, in interfaces.MonoidalCategory]
MonoidalClosureTheory [module, in interfaces.MonoidalCategory]
MonoidalClosureTheory.curry_natural [lemma, in interfaces.MonoidalCategory]
MonoidalDefinition [module, in interfaces.MonoidalCategory]
MonoidalDefinition.Tens [module, in interfaces.MonoidalCategory]
MonoidalFunctor [module, in interfaces.MonoidalCategory]
MonoidalStructure [module, in interfaces.MonoidalCategory]
MonoidalStructureDefinition [module, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.assoc [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.assoc_coh [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.assoc_nat [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.lunit [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.lunit_nat [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.runit [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.runit_nat [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.unit [axiom, in interfaces.MonoidalCategory]
MonoidalStructureDefinition.unit_coh [axiom, in interfaces.MonoidalCategory]
MonoidalStructureTheory [module, in interfaces.MonoidalCategory]
MonoidalStructureTheory.assoc_coh_bw [lemma, in interfaces.MonoidalCategory]
MonoidalStructureTheory.assoc_nat_bw [lemma, in interfaces.MonoidalCategory]
MonoidalStructureTheory.lunit_nat_bw [lemma, in interfaces.MonoidalCategory]
MonoidalStructureTheory.runit_nat_bw [lemma, in interfaces.MonoidalCategory]
MonoidalStructureTheory.unit_coh_bw [lemma, in interfaces.MonoidalCategory]
MonoidalTheory [module, in interfaces.MonoidalCategory]
_ * _ (hom_scope) [notation, in interfaces.MonoidalCategory]
_ * _ (obj_scope) [notation, in interfaces.MonoidalCategory]
1 (obj_scope) [notation, in interfaces.MonoidalCategory]
MonoidalTheory.α [abbreviation, in interfaces.MonoidalCategory]
MonoidalTheory.λ [abbreviation, in interfaces.MonoidalCategory]
MonoidalTheory.ρ [abbreviation, in interfaces.MonoidalCategory]
Monoids [module, in interfaces.FunctorCategory]
Monoids.carrier [projection, in interfaces.FunctorCategory]
Monoids.compose [definition, in interfaces.FunctorCategory]
Monoids.compose_assoc [lemma, in interfaces.FunctorCategory]
Monoids.compose_id_right [lemma, in interfaces.FunctorCategory]
Monoids.compose_id_left [lemma, in interfaces.FunctorCategory]
Monoids.eta [projection, in interfaces.FunctorCategory]
Monoids.id [definition, in interfaces.FunctorCategory]
Monoids.m [definition, in interfaces.FunctorCategory]
Monoids.map [projection, in interfaces.FunctorCategory]
Monoids.map_mu_rewrite [lemma, in interfaces.FunctorCategory]
Monoids.map_eta_rewrite [lemma, in interfaces.FunctorCategory]
Monoids.map_mu [projection, in interfaces.FunctorCategory]
Monoids.map_eta [projection, in interfaces.FunctorCategory]
Monoids.meq [lemma, in interfaces.FunctorCategory]
Monoids.mh [record, in interfaces.FunctorCategory]
Monoids.mon [record, in interfaces.FunctorCategory]
Monoids.mu [projection, in interfaces.FunctorCategory]
Monoids.mu_mu [projection, in interfaces.FunctorCategory]
Monoids.mu_eta_r [projection, in interfaces.FunctorCategory]
Monoids.mu_eta_l [projection, in interfaces.FunctorCategory]
Monoids.t [definition, in interfaces.FunctorCategory]
mor_monotonic [projection, in structures.Poset]
move [inductive, in models.IntStrat]
mtens [projection, in structures.Category]
M_bq [definition, in examples.CAL]
N
N [axiom, in examples.CAL]next [definition, in models.IntStrat]
next_deterministic [instance, in models.IntStrat]
nil_coh_r [constructor, in models.Coherence]
nil_coh_l [constructor, in models.Coherence]
O
oa [constructor, in models.IntStrat]oa_eq_inv [lemma, in models.IntStrat]
oext [definition, in models.Coherence]
oext_uniq [lemma, in models.Coherence]
oext_oret [lemma, in models.Coherence]
omap [definition, in models.Coherence]
omap_compose [lemma, in models.Coherence]
omap_id [lemma, in models.Coherence]
One [module, in interfaces.Category]
One.compose [definition, in interfaces.Category]
One.compose_assoc [lemma, in interfaces.Category]
One.compose_id_right [lemma, in interfaces.Category]
One.compose_id_left [lemma, in interfaces.Category]
One.id [definition, in interfaces.Category]
One.m [definition, in interfaces.Category]
One.t [definition, in interfaces.Category]
op [projection, in models.Signature]
op [projection, in structures.Effects]
op [projection, in models.IntStrat]
operand [projection, in models.Signature]
operand [projection, in models.IntStrat]
operator [projection, in models.Signature]
operator [projection, in models.IntStrat]
OppositeCategory [module, in interfaces.Category]
OppositeCategory.compose [definition, in interfaces.Category]
OppositeCategory.compose_assoc [lemma, in interfaces.Category]
OppositeCategory.compose_id_right [lemma, in interfaces.Category]
OppositeCategory.compose_id_left [lemma, in interfaces.Category]
OppositeCategory.id [definition, in interfaces.Category]
OppositeCategory.m [definition, in interfaces.Category]
OppositeCategory.t [definition, in interfaces.Category]
OPS [section, in structures.Lattice]
op_mor [projection, in structures.Effects]
op_lm [projection, in structures.Effects]
oq [constructor, in models.IntStrat]
oret [definition, in models.Coherence]
output [definition, in models.Coherence]
P
pa [constructor, in models.IntStrat]PartialOrder [record, in models.DCPO]
passoc [definition, in models.IntStrat]
passoc_pswap [lemma, in models.IntStrat]
passoc_passoc [lemma, in models.IntStrat]
pa_eq_inv [lemma, in models.IntStrat]
pcoh [inductive, in models.IntStrat]
pcoh_inv_pa [lemma, in models.IntStrat]
pcoh_inv_pq [lemma, in models.IntStrat]
pcoh_sym [instance, in models.IntStrat]
pcoh_refl [instance, in models.IntStrat]
pcons [constructor, in models.IntStrat]
pcons_pcoh_oa [constructor, in models.IntStrat]
pcons_pcoh_oq [constructor, in models.IntStrat]
pcons_pcoh [constructor, in models.IntStrat]
pcons_pa_inv [lemma, in models.IntStrat]
pcons_oa_inv [lemma, in models.IntStrat]
pcons_eq_inv_r [lemma, in models.IntStrat]
pcons_eq_inv_l [lemma, in models.IntStrat]
pcons_pref [constructor, in models.IntStrat]
play [inductive, in models.IntStrat]
play_poset [definition, in models.IntStrat]
plu [definition, in models.IntStrat]
plu_pswap [lemma, in models.IntStrat]
plu_passoc [lemma, in models.IntStrat]
pnil_suspended_pcoh_r [constructor, in models.IntStrat]
pnil_suspended_pcoh_l [constructor, in models.IntStrat]
pnil_ready_pcoh_r [constructor, in models.IntStrat]
pnil_ready_pcoh_l [constructor, in models.IntStrat]
pnil_suspended_pref [constructor, in models.IntStrat]
pnil_ready_pref [constructor, in models.IntStrat]
pnil_suspended [constructor, in models.IntStrat]
pnil_ready [constructor, in models.IntStrat]
Poset [module, in models.DCPO]
poset [record, in structures.Poset]
Poset [library]
PosetMorphism [record, in structures.Poset]
poset_prod [definition, in lattices.LatticeProduct]
poset_carrier [projection, in structures.Poset]
Poset.compose_mor [instance, in models.DCPO]
Poset.id_mor [instance, in models.DCPO]
Poset.Morphism [definition, in models.DCPO]
Poset.Structure [definition, in models.DCPO]
position [inductive, in models.IntStrat]
pq [constructor, in models.IntStrat]
PREDICATES [section, in structures.Lattice]
pref [inductive, in models.IntStrat]
prefix_coh [lemma, in models.Coherence]
pref_refl [lemma, in models.IntStrat]
PreservesProducts [module, in interfaces.Limits]
PreservesProducts.fmap_pi [axiom, in interfaces.Limits]
PreservesProducts.omap_prod [axiom, in interfaces.Limits]
Prod [module, in interfaces.Category]
Products [module, in interfaces.Limits]
ProductsDefinition [module, in interfaces.Limits]
ProductsDefinition.pi [axiom, in interfaces.Limits]
ProductsDefinition.pi_tuple [axiom, in interfaces.Limits]
ProductsDefinition.prod [axiom, in interfaces.Limits]
ProductsDefinition.tuple [axiom, in interfaces.Limits]
ProductsDefinition.tuple_pi [axiom, in interfaces.Limits]
ProductsTheory [module, in interfaces.Limits]
ProductsTheory.pi_tuple_rewrite [lemma, in interfaces.Limits]
ProductsTheory.tuple_uni [lemma, in interfaces.Limits]
prod_lens [definition, in models.IntStrat]
prod_bij_bcomp [lemma, in models.IntStrat]
prod_bij_id [lemma, in models.IntStrat]
prod_bij [definition, in models.IntStrat]
Prod.compose [definition, in interfaces.Category]
Prod.compose_assoc [lemma, in interfaces.Category]
Prod.compose_id_right [lemma, in interfaces.Category]
Prod.compose_id_left [lemma, in interfaces.Category]
Prod.id [definition, in interfaces.Category]
Prod.m [definition, in interfaces.Category]
Prod.t [definition, in interfaces.Category]
PROPERTIES [section, in structures.Lattice]
pru [definition, in models.IntStrat]
pswap [definition, in models.IntStrat]
pswap_pswap [lemma, in models.IntStrat]
R
rb_bq [inductive, in examples.CAL]rb_state [definition, in examples.CAL]
rb_sig [inductive, in examples.CAL]
RC [section, in models.IntStrat]
rcnext [definition, in models.IntStrat]
rcnext_lcj [lemma, in models.IntStrat]
rcnext_lcp [lemma, in models.IntStrat]
rcnext_tconv [lemma, in models.IntStrat]
rcnext_fcomp_r [lemma, in models.IntStrat]
rcnext_fcomp_l [lemma, in models.IntStrat]
rcnext_emor [lemma, in models.IntStrat]
rcnext_vcomp_at [lemma, in models.IntStrat]
rcnext_vid [lemma, in models.IntStrat]
rcnext_params [instance, in models.IntStrat]
rcnext_sup [lemma, in models.IntStrat]
rcnext_inf [lemma, in models.IntStrat]
rcnext_ref [instance, in models.IntStrat]
rcp [inductive, in models.IntStrat]
rcp_poset [definition, in models.IntStrat]
rcp_forbid_ref [constructor, in models.IntStrat]
rcp_cont_forbid_ref [constructor, in models.IntStrat]
rcp_cont_ref [constructor, in models.IntStrat]
rcp_allow_forbid_ref [constructor, in models.IntStrat]
rcp_allow_cont_ref [constructor, in models.IntStrat]
rcp_allow_ref [constructor, in models.IntStrat]
rcp_ref [inductive, in models.IntStrat]
rcp_cont [constructor, in models.IntStrat]
rcp_forbid [constructor, in models.IntStrat]
rcp_allow [constructor, in models.IntStrat]
ready [constructor, in models.IntStrat]
ref [definition, in models.Coherence]
ref [projection, in structures.Poset]
ref_meet [lemma, in structures.Lattice]
ref_join [lemma, in structures.Lattice]
ref_po [instance, in models.Coherence]
ref_preo [instance, in models.Coherence]
ref_po [projection, in structures.Poset]
ref_preo [projection, in structures.Poset]
Reg [module, in models.EffectSignatures]
RegBase [module, in models.EffectSignatures]
RegBase.compose [definition, in models.EffectSignatures]
RegBase.compose_assoc [lemma, in models.EffectSignatures]
RegBase.compose_id_right [lemma, in models.EffectSignatures]
RegBase.compose_id_left [lemma, in models.EffectSignatures]
RegBase.id [definition, in models.EffectSignatures]
RegBase.m [definition, in models.EffectSignatures]
RegBase.t [definition, in models.EffectSignatures]
RegBase.transform [definition, in models.EffectSignatures]
RegBase.transform_compose [lemma, in models.EffectSignatures]
RegBase.transform_id [lemma, in models.EffectSignatures]
RegPlus [module, in models.EffectSignatures]
RegPlusReq [module, in models.EffectSignatures]
RegPlus.Plus [module, in models.EffectSignatures]
RegPlus.Plus.copair [definition, in models.EffectSignatures]
RegPlus.Plus.copair_iota_compose [lemma, in models.EffectSignatures]
RegPlus.Plus.copair_i2 [lemma, in models.EffectSignatures]
RegPlus.Plus.copair_i1 [lemma, in models.EffectSignatures]
RegPlus.Plus.ini [definition, in models.EffectSignatures]
RegPlus.Plus.ini_uni [lemma, in models.EffectSignatures]
RegPlus.Plus.i1 [definition, in models.EffectSignatures]
RegPlus.Plus.i2 [definition, in models.EffectSignatures]
RegPlus.Plus.omap [definition, in models.EffectSignatures]
RegPlus.Plus.unit [definition, in models.EffectSignatures]
RegSpec [module, in models.EffectSignatures]
ret [projection, in structures.Monad]
retract [lemma, in models.IntStrat]
retraction [projection, in models.IntStrat]
Retraction [record, in models.IntStrat]
ret_bind [projection, in structures.Monad]
rscpos [inductive, in models.IntStrat]
rsc_suspended [constructor, in models.IntStrat]
rsc_right [constructor, in models.IntStrat]
rsc_left [constructor, in models.IntStrat]
rsc_ready [constructor, in models.IntStrat]
rsp [inductive, in models.IntStrat]
rspos [inductive, in models.IntStrat]
rsp_vcomp [lemma, in models.IntStrat]
rsp_comp [lemma, in models.IntStrat]
rsp_params [instance, in models.IntStrat]
rsp_inf [lemma, in models.IntStrat]
rsp_sup [lemma, in models.IntStrat]
rsp_sup_cases [lemma, in models.IntStrat]
rsp_suspended_inv_nil [lemma, in models.IntStrat]
rsp_ready_inv_nil [lemma, in models.IntStrat]
rsp_ref [instance, in models.IntStrat]
rsp_pa [constructor, in models.IntStrat]
rsp_oa [constructor, in models.IntStrat]
rsp_suspended [constructor, in models.IntStrat]
rsp_pq [constructor, in models.IntStrat]
rsp_oq [constructor, in models.IntStrat]
rsp_ready [constructor, in models.IntStrat]
rsq [definition, in models.IntStrat]
RSQ [section, in models.IntStrat]
rsq_vcomp [lemma, in models.IntStrat]
rsq_vcomp_when [lemma, in models.IntStrat]
rsq_comp [lemma, in models.IntStrat]
rsq_comp_when [lemma, in models.IntStrat]
RSQ_COMP [section, in models.IntStrat]
rsq_params [instance, in models.IntStrat]
rsq_when_params [instance, in models.IntStrat]
rsq_sup [lemma, in models.IntStrat]
rsq_next_pa [lemma, in models.IntStrat]
rsq_next_oa [lemma, in models.IntStrat]
rsq_next_pq [lemma, in models.IntStrat]
rsq_next_oq [lemma, in models.IntStrat]
rsq_ref [instance, in models.IntStrat]
rsq_when_ref [instance, in models.IntStrat]
rsq_when [definition, in models.IntStrat]
RSVCOMP [section, in models.IntStrat]
rsvpos [inductive, in models.IntStrat]
rsv_suspended [constructor, in models.IntStrat]
rsv_running [constructor, in models.IntStrat]
rsv_ready [constructor, in models.IntStrat]
rs_suspended [constructor, in models.IntStrat]
rs_running [constructor, in models.IntStrat]
rs_ready [constructor, in models.IntStrat]
running [constructor, in models.IntStrat]
S
sassoc [definition, in models.IntStrat]sassocr [definition, in models.IntStrat]
sassoc_iso [instance, in models.IntStrat]
sccpos [inductive, in models.IntStrat]
scc_suspended [constructor, in models.IntStrat]
scc_right [constructor, in models.IntStrat]
scc_left [constructor, in models.IntStrat]
scc_ready [constructor, in models.IntStrat]
scipos [inductive, in models.IntStrat]
sci_suspended [constructor, in models.IntStrat]
sci_ready [constructor, in models.IntStrat]
scomp [definition, in models.IntStrat]
scomp_vcomp [lemma, in models.IntStrat]
scomp_vid [lemma, in models.IntStrat]
scomp_compose [lemma, in models.IntStrat]
scomp_compose_when_2 [lemma, in models.IntStrat]
scomp_compose_when_1 [lemma, in models.IntStrat]
SCOMP_COMPOSE [section, in models.IntStrat]
scomp_id [lemma, in models.IntStrat]
scomp_id_when [lemma, in models.IntStrat]
SCOMP_ID [section, in models.IntStrat]
scomp_rsq [lemma, in models.IntStrat]
scomp_conv [definition, in models.IntStrat]
scomp_strat_eq [instance, in models.IntStrat]
scomp_strat [definition, in models.IntStrat]
scons [definition, in models.IntStrat]
scons_next_adj [lemma, in models.IntStrat]
scons_deterministic [instance, in models.IntStrat]
ScottContinuous [record, in models.DCPO]
sc_dsup [lemma, in models.DCPO]
sc_le [instance, in models.DCPO]
sc_dsup_sup [projection, in models.DCPO]
seq [definition, in models.Coherence]
seq_lmap [definition, in models.Coherence]
SET [instance, in structures.Category]
set [constructor, in examples.CAL]
SET [module, in models.Sets]
set [constructor, in models.Signature]
SET [module, in interfaces.Category]
set [projection, in models.IntStrat]
SetBase [module, in models.Sets]
SetBaseSpec [module, in models.Sets]
SetBase.compose [definition, in models.Sets]
SetBase.compose_assoc [lemma, in models.Sets]
SetBase.compose_id_right [lemma, in models.Sets]
SetBase.compose_id_left [lemma, in models.Sets]
SetBase.id [definition, in models.Sets]
SetBase.m [definition, in models.Sets]
SetBase.natural [lemma, in models.Sets]
SetBase.t [definition, in models.Sets]
SetMonoidalStructures [module, in models.Sets]
SetMonoidalStructures.Exp [module, in models.Sets]
SetMonoidalStructures.Exp.curry [definition, in models.Sets]
SetMonoidalStructures.Exp.curry_natural_r [lemma, in models.Sets]
SetMonoidalStructures.Exp.curry_natural_l [lemma, in models.Sets]
SetMonoidalStructures.Exp.curry_uncurry [lemma, in models.Sets]
SetMonoidalStructures.Exp.fmap [definition, in models.Sets]
SetMonoidalStructures.Exp.fmap_compose [lemma, in models.Sets]
SetMonoidalStructures.Exp.fmap_id [lemma, in models.Sets]
SetMonoidalStructures.Exp.omap [definition, in models.Sets]
SetMonoidalStructures.Exp.uncurry [definition, in models.Sets]
SetMonoidalStructures.Exp.uncurry_curry [lemma, in models.Sets]
SetMonoidalStructures.Prod [module, in models.Sets]
SetMonoidalStructures.Prod.omap [definition, in models.Sets]
SetMonoidalStructures.Prod.pair [definition, in models.Sets]
SetMonoidalStructures.Prod.pair_pi_compose [lemma, in models.Sets]
SetMonoidalStructures.Prod.p1 [definition, in models.Sets]
SetMonoidalStructures.Prod.p1_pair [lemma, in models.Sets]
SetMonoidalStructures.Prod.p2 [definition, in models.Sets]
SetMonoidalStructures.Prod.p2_pair [lemma, in models.Sets]
SetMonoidalStructures.Prod.ter [definition, in models.Sets]
SetMonoidalStructures.Prod.ter_uni [lemma, in models.Sets]
SetMonoidalStructures.Prod.unit [definition, in models.Sets]
Sets [library]
SetSpec [module, in models.Sets]
SET_prod [instance, in structures.Category]
set_eqv [projection, in models.IntStrat]
set_set [projection, in models.IntStrat]
set_get [projection, in models.IntStrat]
SET.compose [definition, in interfaces.Category]
SET.compose_assoc [lemma, in interfaces.Category]
SET.compose_id_right [lemma, in interfaces.Category]
SET.compose_id_left [lemma, in interfaces.Category]
SET.id [definition, in interfaces.Category]
SET.m [definition, in interfaces.Category]
SET.t [definition, in interfaces.Category]
Sig [module, in models.EffectSignatures]
sig [record, in models.Signature]
SigBase [module, in models.EffectSignatures]
SigBase.amap [definition, in models.EffectSignatures]
SigBase.amap_compose [lemma, in models.EffectSignatures]
SigBase.amap_id [lemma, in models.EffectSignatures]
SigBase.application [record, in models.EffectSignatures]
SigBase.apply [constructor, in models.EffectSignatures]
SigBase.ar [projection, in models.EffectSignatures]
SigBase.compose [definition, in models.EffectSignatures]
SigBase.compose_assoc [lemma, in models.EffectSignatures]
SigBase.compose_id_right [lemma, in models.EffectSignatures]
SigBase.compose_id_left [lemma, in models.EffectSignatures]
SigBase.cons [constructor, in models.EffectSignatures]
SigBase.coprod [definition, in models.EffectSignatures]
SigBase.cotuple [definition, in models.EffectSignatures]
SigBase.cotuple_iota [lemma, in models.EffectSignatures]
SigBase.ear [definition, in models.EffectSignatures]
SigBase.eop [inductive, in models.EffectSignatures]
SigBase.esig [definition, in models.EffectSignatures]
SigBase.esig_sig [definition, in models.EffectSignatures]
SigBase.hmap [definition, in models.EffectSignatures]
SigBase.hmap_compose [lemma, in models.EffectSignatures]
SigBase.hmap_id [lemma, in models.EffectSignatures]
SigBase.hmap_natural [lemma, in models.EffectSignatures]
SigBase.id [definition, in models.EffectSignatures]
SigBase.iota [definition, in models.EffectSignatures]
SigBase.iota_cotuple [lemma, in models.EffectSignatures]
SigBase.m [definition, in models.EffectSignatures]
SigBase.mkop [constructor, in models.EffectSignatures]
SigBase.mkops [constructor, in models.EffectSignatures]
SigBase.op [projection, in models.EffectSignatures]
SigBase.operand [projection, in models.EffectSignatures]
SigBase.operator [projection, in models.EffectSignatures]
SigBase.ops [record, in models.EffectSignatures]
SigBase.pi [definition, in models.EffectSignatures]
SigBase.pi_tuple [lemma, in models.EffectSignatures]
SigBase.prod [definition, in models.EffectSignatures]
SigBase.prod_op [projection, in models.EffectSignatures]
SigBase.sig [record, in models.EffectSignatures]
SigBase.sig_esig_op [constructor, in models.EffectSignatures]
SigBase.sig_esig [inductive, in models.EffectSignatures]
SigBase.subst [definition, in models.EffectSignatures]
SigBase.subst_expand [lemma, in models.EffectSignatures]
SigBase.subst_tmap [lemma, in models.EffectSignatures]
SigBase.subst_subst [lemma, in models.EffectSignatures]
SigBase.subst_cons [lemma, in models.EffectSignatures]
SigBase.subst_var_r [lemma, in models.EffectSignatures]
SigBase.subst_var_l [lemma, in models.EffectSignatures]
SigBase.t [definition, in models.EffectSignatures]
SigBase.term [inductive, in models.EffectSignatures]
SigBase.tmap [definition, in models.EffectSignatures]
SigBase.tmap_tmul [lemma, in models.EffectSignatures]
SigBase.tmap_cons [lemma, in models.EffectSignatures]
SigBase.tmap_var [lemma, in models.EffectSignatures]
SigBase.tmap_compose [lemma, in models.EffectSignatures]
SigBase.tmap_id [lemma, in models.EffectSignatures]
SigBase.tmul [definition, in models.EffectSignatures]
SigBase.tmul_var_r [lemma, in models.EffectSignatures]
SigBase.tmul_var_l [lemma, in models.EffectSignatures]
SigBase.tmul_natural [lemma, in models.EffectSignatures]
SigBase.transform [definition, in models.EffectSignatures]
SigBase.transform_compose [lemma, in models.EffectSignatures]
SigBase.transform_id [lemma, in models.EffectSignatures]
SigBase.tuple [definition, in models.EffectSignatures]
SigBase.tuple_pi [lemma, in models.EffectSignatures]
SigBase.var [constructor, in models.EffectSignatures]
_ >= _ => _ (appl_scope) [notation, in models.EffectSignatures]
_ >= _ => _ (term_scope) [notation, in models.EffectSignatures]
SigComp [module, in models.EffectSignatures]
sigcomp [definition, in models.Signature]
sigcomp_assoc [lemma, in models.Signature]
sigcomp_id_r [lemma, in models.Signature]
sigcomp_id_l [lemma, in models.Signature]
SigComp.Comp [module, in models.EffectSignatures]
SigComp.Comp.aeq [lemma, in models.EffectSignatures]
SigComp.Comp.aeq' [lemma, in models.EffectSignatures]
SigComp.Comp.ar [record, in models.EffectSignatures]
SigComp.Comp.ar_next [projection, in models.EffectSignatures]
SigComp.Comp.ar_first [projection, in models.EffectSignatures]
SigComp.Comp.assoc [definition, in models.EffectSignatures]
SigComp.Comp.assoc_coh [lemma, in models.EffectSignatures]
SigComp.Comp.assoc_nat [lemma, in models.EffectSignatures]
SigComp.Comp.fmap [definition, in models.EffectSignatures]
SigComp.Comp.fmap_compose [lemma, in models.EffectSignatures]
SigComp.Comp.fmap_id [lemma, in models.EffectSignatures]
SigComp.Comp.lunit [definition, in models.EffectSignatures]
SigComp.Comp.lunit_nat [lemma, in models.EffectSignatures]
SigComp.Comp.mkar [constructor, in models.EffectSignatures]
SigComp.Comp.mkop [constructor, in models.EffectSignatures]
SigComp.Comp.omap [definition, in models.EffectSignatures]
SigComp.Comp.op [record, in models.EffectSignatures]
SigComp.Comp.op_next [projection, in models.EffectSignatures]
SigComp.Comp.op_first [projection, in models.EffectSignatures]
SigComp.Comp.runit [definition, in models.EffectSignatures]
SigComp.Comp.runit_nat [lemma, in models.EffectSignatures]
SigComp.Comp.unit [definition, in models.EffectSignatures]
SigComp.Comp.unit_coh [lemma, in models.EffectSignatures]
_ ⊳ _ (hom_scope) [notation, in models.EffectSignatures]
_ ⊳ _ (obj_scope) [notation, in models.EffectSignatures]
SigEnd [module, in models.EffectSignatures]
SigEnd.faithful [lemma, in models.EffectSignatures]
SigEnd.fmap [definition, in models.EffectSignatures]
SigEnd.fmap_compose [lemma, in models.EffectSignatures]
SigEnd.fmap_id [lemma, in models.EffectSignatures]
SigEnd.full [lemma, in models.EffectSignatures]
SigEnd.omap [definition, in models.EffectSignatures]
sighom [definition, in models.Signature]
sigi [definition, in models.Signature]
sigid [definition, in models.Signature]
siginl [definition, in models.Signature]
siginr [definition, in models.Signature]
SigMnd [module, in models.EffectSignatures]
SigMnd.faithful [lemma, in models.EffectSignatures]
SigMnd.fmap [definition, in models.EffectSignatures]
SigMnd.fmap_compose [lemma, in models.EffectSignatures]
SigMnd.fmap_id [lemma, in models.EffectSignatures]
SigMnd.full [lemma, in models.EffectSignatures]
SigMnd.map_cons [lemma, in models.EffectSignatures]
SigMnd.map_var [lemma, in models.EffectSignatures]
SigMnd.omap [definition, in models.EffectSignatures]
Signature [library]
sigo [definition, in models.Signature]
SigPlus [module, in models.EffectSignatures]
SigPlusReq [module, in models.EffectSignatures]
SigPlus.Plus [module, in models.EffectSignatures]
SigPlus.Plus.copair [definition, in models.EffectSignatures]
SigPlus.Plus.copair_iota_compose [lemma, in models.EffectSignatures]
SigPlus.Plus.copair_i2 [lemma, in models.EffectSignatures]
SigPlus.Plus.copair_i1 [lemma, in models.EffectSignatures]
SigPlus.Plus.ini [definition, in models.EffectSignatures]
SigPlus.Plus.ini_uni [lemma, in models.EffectSignatures]
SigPlus.Plus.i1 [definition, in models.EffectSignatures]
SigPlus.Plus.i2 [definition, in models.EffectSignatures]
SigPlus.Plus.omap [definition, in models.EffectSignatures]
SigPlus.Plus.unit [definition, in models.EffectSignatures]
SigReg [module, in models.EffectSignatures]
SigReg.faithful [lemma, in models.EffectSignatures]
SigReg.fmap [definition, in models.EffectSignatures]
SigReg.fmap_compose [lemma, in models.EffectSignatures]
SigReg.fmap_id [lemma, in models.EffectSignatures]
SigReg.omap [definition, in models.EffectSignatures]
SigSpec [module, in models.EffectSignatures]
sigsum [definition, in models.Signature]
SigTens [module, in models.EffectSignatures]
sigtens [definition, in models.Signature]
SigTensReq [module, in models.EffectSignatures]
SigTens.Tens [module, in models.EffectSignatures]
SigTens.Tens.assoc [definition, in models.EffectSignatures]
SigTens.Tens.assoc_coh [lemma, in models.EffectSignatures]
SigTens.Tens.assoc_nat [lemma, in models.EffectSignatures]
SigTens.Tens.fmap [definition, in models.EffectSignatures]
SigTens.Tens.fmap_compose [lemma, in models.EffectSignatures]
SigTens.Tens.fmap_id [lemma, in models.EffectSignatures]
SigTens.Tens.lunit [definition, in models.EffectSignatures]
SigTens.Tens.lunit_nat [lemma, in models.EffectSignatures]
SigTens.Tens.omap [definition, in models.EffectSignatures]
SigTens.Tens.runit [definition, in models.EffectSignatures]
SigTens.Tens.runit_swap [lemma, in models.EffectSignatures]
SigTens.Tens.runit_nat [lemma, in models.EffectSignatures]
SigTens.Tens.swap [definition, in models.EffectSignatures]
SigTens.Tens.swap_swap [lemma, in models.EffectSignatures]
SigTens.Tens.swap_assoc [lemma, in models.EffectSignatures]
SigTens.Tens.swap_nat [lemma, in models.EffectSignatures]
SigTens.Tens.unit [definition, in models.EffectSignatures]
SigTens.Tens.unit_coh [lemma, in models.EffectSignatures]
_ * _ (hom_scope) [notation, in models.EffectSignatures]
_ * _ (obj_scope) [notation, in models.EffectSignatures]
sigtup [definition, in models.Signature]
sigtup_uniq [lemma, in models.Signature]
sigtup_inr [lemma, in models.Signature]
sigtup_inl [lemma, in models.Signature]
slens_eqv_equiv [instance, in models.IntStrat]
slice [definition, in examples.CAL]
slice_length [lemma, in examples.CAL]
slift [definition, in examples.CAL]
slu [definition, in models.IntStrat]
slur [definition, in models.IntStrat]
slu_iso [instance, in models.IntStrat]
SMCat [record, in structures.Category]
SMnd [module, in models.Sets]
space [record, in models.Coherence]
srel_push_pull [lemma, in examples.CAL]
srel_pull [definition, in examples.CAL]
srel_push [definition, in examples.CAL]
sru [definition, in models.IntStrat]
srun [definition, in examples.CAL]
srunpos [inductive, in models.IntStrat]
srun_int [lemma, in examples.CAL]
srun_bind [lemma, in examples.CAL]
srun_slift [lemma, in examples.CAL]
srun_suspended [constructor, in models.IntStrat]
srun_running [constructor, in models.IntStrat]
srun_ready [constructor, in models.IntStrat]
srur [definition, in models.IntStrat]
srur_natural [lemma, in models.IntStrat]
sru_natural [lemma, in models.IntStrat]
sru_natural_has_2 [lemma, in models.IntStrat]
sru_natural_has_1 [lemma, in models.IntStrat]
SRU_NATURAL [section, in models.IntStrat]
sru_iso [instance, in models.IntStrat]
st [constructor, in examples.CAL]
state [projection, in models.IntStrat]
stateful_play_mor [instance, in examples.CAL]
stateful_play [definition, in examples.CAL]
state_sig [inductive, in examples.CAL]
state_eqv [projection, in models.IntStrat]
strat [definition, in models.IntStrat]
STRAT [section, in models.IntStrat]
strat_has_any_pnil_suspended [lemma, in models.IntStrat]
strat_has_any_pnil_ready [lemma, in models.IntStrat]
strat_closed [lemma, in models.IntStrat]
STRAT.NEXT [section, in models.IntStrat]
subst [definition, in models.Sets]
suffix_coh [lemma, in models.Coherence]
sum_inr_coh [constructor, in models.Coherence]
sum_inl_coh [constructor, in models.Coherence]
Sup [module, in lattices.Downset]
sup_iff [lemma, in structures.Lattice]
sup_at [lemma, in structures.Lattice]
sup_inf [projection, in structures.Lattice]
sup_lub [projection, in structures.Lattice]
sup_ub [projection, in structures.Lattice]
sup_unique [lemma, in models.DCPO]
sup_lub [projection, in models.DCPO]
sup_ub [projection, in models.DCPO]
sup_eq [instance, in models.IntStrat]
Sup.compose_mor [lemma, in lattices.Downset]
Sup.id_mor [lemma, in lattices.Downset]
Sup.mor [projection, in lattices.Downset]
Sup.mor [constructor, in lattices.Downset]
Sup.Morphism [record, in lattices.Downset]
Sup.Morphism [inductive, in lattices.Downset]
Sup.mor_bot [lemma, in lattices.Downset]
Sup.mor_ref [lemma, in lattices.Downset]
Sup.mor_join [lemma, in lattices.Downset]
suspended [constructor, in models.IntStrat]
SymmetricMonoidal [module, in interfaces.MonoidalCategory]
SymmetricMonoidalCategory [module, in interfaces.MonoidalCategory]
SymmetricMonoidalDefinition [module, in interfaces.MonoidalCategory]
SymmetricMonoidalDefinition.Tens [module, in interfaces.MonoidalCategory]
SymmetricMonoidalStructure [module, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition [module, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.runit_swap [axiom, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap [axiom, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap_swap [axiom, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap_assoc [axiom, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap_nat [axiom, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory [module, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.lunit_swap_bw [lemma, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.lunit_swap [lemma, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.runit_swap_bw [lemma, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.swap_assoc_bw [lemma, in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.swap_iso [definition, in interfaces.MonoidalCategory]
SymmetricMonoidalTheory [module, in interfaces.MonoidalCategory]
SymmetricMonoidalTheory.γ [abbreviation, in interfaces.MonoidalCategory]
T
tassoc [definition, in models.IntStrat]tassocr [definition, in models.IntStrat]
tassocr_tassoc [lemma, in models.IntStrat]
tassoc_tswap [lemma, in models.IntStrat]
tassoc_tassoc [lemma, in models.IntStrat]
tassoc_tassocr [lemma, in models.IntStrat]
tconv [definition, in models.IntStrat]
TCONV [section, in models.IntStrat]
tconv_vid [lemma, in models.IntStrat]
tconv_vcomp [lemma, in models.IntStrat]
tconv_vcomp_at [lemma, in models.IntStrat]
TCONV_VCOMP [section, in models.IntStrat]
tconv_inf_r [lemma, in models.IntStrat]
tconv_inf_l [lemma, in models.IntStrat]
tconv_sup [lemma, in models.IntStrat]
tconv_sup_r [lemma, in models.IntStrat]
tconv_sup_l [lemma, in models.IntStrat]
tconv_has [definition, in models.IntStrat]
tens [projection, in structures.Category]
tens [definition, in models.IntStrat]
tens_compose [lemma, in models.IntStrat]
tens_eid [lemma, in models.IntStrat]
tens_emor [definition, in models.IntStrat]
TENS_EMOR [section, in models.IntStrat]
term [inductive, in models.Sets]
test [definition, in models.Sets]
testsig [inductive, in models.Sets]
tlu [definition, in models.IntStrat]
tlur [definition, in models.IntStrat]
tlur_tlu [lemma, in models.IntStrat]
tlu_tswap [lemma, in models.IntStrat]
tlu_tassoc [lemma, in models.IntStrat]
tlu_tlur [lemma, in models.IntStrat]
tmap [definition, in models.Sets]
tmap_compose [lemma, in models.Sets]
tmap_id [lemma, in models.Sets]
token [projection, in models.Coherence]
top [definition, in structures.Lattice]
top_ub [lemma, in structures.Lattice]
tpos [inductive, in models.IntStrat]
tp_suspended [constructor, in models.IntStrat]
tp_running [constructor, in models.IntStrat]
tp_ready [constructor, in models.IntStrat]
trsp [lemma, in models.IntStrat]
trspos [inductive, in models.IntStrat]
trsq [lemma, in models.IntStrat]
TRSQ [section, in models.IntStrat]
trs_suspended [constructor, in models.IntStrat]
trs_running [constructor, in models.IntStrat]
trs_ready [constructor, in models.IntStrat]
tru [definition, in models.IntStrat]
trur [definition, in models.IntStrat]
trur_tru [lemma, in models.IntStrat]
tru_trur [lemma, in models.IntStrat]
tstrat [abbreviation, in models.IntStrat]
TSTRAT [section, in models.IntStrat]
tstrat_next_pa [lemma, in models.IntStrat]
tstrat_next_oa [lemma, in models.IntStrat]
tstrat_next_pq [lemma, in models.IntStrat]
tstrat_next_oq [lemma, in models.IntStrat]
tstrat_when [definition, in models.IntStrat]
tstrat_has_pa [constructor, in models.IntStrat]
tstrat_has_oa [constructor, in models.IntStrat]
tstrat_has_suspended [constructor, in models.IntStrat]
tstrat_has_pq [constructor, in models.IntStrat]
tstrat_has_oq [constructor, in models.IntStrat]
tstrat_has_ready [constructor, in models.IntStrat]
tstrat_has [inductive, in models.IntStrat]
tswap [definition, in models.IntStrat]
tswap_tswap [lemma, in models.IntStrat]
Two [module, in interfaces.Category]
Two.compose [definition, in interfaces.Category]
Two.compose_assoc [lemma, in interfaces.Category]
Two.compose_id_right [lemma, in interfaces.Category]
Two.compose_id_left [lemma, in interfaces.Category]
Two.id [definition, in interfaces.Category]
Two.id_def [constructor, in interfaces.Category]
Two.int [constructor, in interfaces.Category]
Two.m [definition, in interfaces.Category]
Two.m_def [inductive, in interfaces.Category]
Two.t [definition, in interfaces.Category]
U
Unnamed_thm [definition, in examples.CAL]up [abbreviation, in lattices.Upset]
update [definition, in examples.CAL]
upset [abbreviation, in lattices.Upset]
Upset [module, in lattices.Upset]
Upset [library]
Upset.DEFS [section, in lattices.Upset]
Upset.emb [definition, in lattices.Upset]
Upset.emb_mor [lemma, in lattices.Upset]
Upset.ext [definition, in lattices.Upset]
Upset.ext_unique [lemma, in lattices.Upset]
Upset.ext_ana [lemma, in lattices.Upset]
Upset.ext_mor [instance, in lattices.Upset]
Upset.F [definition, in lattices.Upset]
Upset.opp_cdlat [definition, in lattices.Upset]
Upset.opp_poset [definition, in lattices.Upset]
V
val [axiom, in examples.CAL]var [constructor, in models.Sets]
vcomp [definition, in models.IntStrat]
VCOMP [section, in models.IntStrat]
VCOMP_NOT_ASSOC.vcomp_not_assoc [lemma, in models.IntStrat]
VCOMP_NOT_ASSOC.S [definition, in models.IntStrat]
VCOMP_NOT_ASSOC.foo [definition, in models.IntStrat]
VCOMP_NOT_ASSOC.R [definition, in models.IntStrat]
VCOMP_NOT_ASSOC.foo_cont [constructor, in models.IntStrat]
VCOMP_NOT_ASSOC.foo_r [constructor, in models.IntStrat]
VCOMP_NOT_ASSOC.foo_q [constructor, in models.IntStrat]
VCOMP_NOT_ASSOC.foo_has [inductive, in models.IntStrat]
VCOMP_NOT_ASSOC.toprc_has [definition, in models.IntStrat]
VCOMP_NOT_ASSOC.twoq [definition, in models.IntStrat]
VCOMP_NOT_ASSOC.twoa [definition, in models.IntStrat]
VCOMP_NOT_ASSOC.one [definition, in models.IntStrat]
VCOMP_NOT_ASSOC [module, in models.IntStrat]
vcomp_vid_r [lemma, in models.IntStrat]
vcomp_vid_l [lemma, in models.IntStrat]
VCOMP_VID [section, in models.IntStrat]
vcomp_expand [lemma, in models.IntStrat]
vcomp_at [definition, in models.IntStrat]
vcomp_at_has [definition, in models.IntStrat]
vcomp_has_ref [instance, in models.IntStrat]
vcomp_has [definition, in models.IntStrat]
vid [definition, in models.IntStrat]
VID [section, in models.IntStrat]
vid_has [definition, in models.IntStrat]
Z
Zero [module, in interfaces.Category]Zero.compose [definition, in interfaces.Category]
Zero.compose_assoc [lemma, in interfaces.Category]
Zero.compose_id_right [lemma, in interfaces.Category]
Zero.compose_id_left [lemma, in interfaces.Category]
Zero.id [definition, in interfaces.Category]
Zero.m [definition, in interfaces.Category]
Zero.t [definition, in interfaces.Category]
other
_ * _ (bijection_scope) [notation, in models.IntStrat]_ ∘ _ (bijection_scope) [notation, in models.IntStrat]
_ ^ _ (cdlat_scope) [notation, in lattices.LatticeProduct]
pi _ .. _ , _ (cdlat_scope) [notation, in lattices.LatticeProduct]
! _ (clique_scope) [notation, in models.Coherence]
_ * _ (clique_scope) [notation, in models.Coherence]
[ _ , _ ] (clique_scope) [notation, in models.Coherence]
{ _ , _ } (clique_scope) [notation, in models.Coherence]
_ @ _ (clique_scope) [notation, in models.Coherence]
! _ (coh_scope) [notation, in models.Coherence]
_ ;; _ (coh_scope) [notation, in models.Coherence]
1 (coh_scope) [notation, in models.Coherence]
_ * _ (coh_scope) [notation, in models.Coherence]
_ + _ (coh_scope) [notation, in models.Coherence]
_ && _ (coh_scope) [notation, in models.Coherence]
_ --o _ (coh_scope) [notation, in models.Coherence]
_ @ _ (conv_scope) [notation, in models.IntStrat]
_ * _ (conv_scope) [notation, in models.IntStrat]
_ + _ (conv_scope) [notation, in models.IntStrat]
_ ;; _ (conv_scope) [notation, in models.IntStrat]
_ * _ (emor_scope) [notation, in models.IntStrat]
_ + _ (emor_scope) [notation, in models.IntStrat]
_ ∘ _ (emor_scope) [notation, in models.IntStrat]
_ + _ (esig_scope) [notation, in structures.Effects]
_ @ _ (esig_scope) [notation, in models.IntStrat]
_ * _ (esig_scope) [notation, in models.IntStrat]
1 (esig_scope) [notation, in models.IntStrat]
0 (esig_scope) [notation, in models.IntStrat]
_ + _ (esig_scope) [notation, in models.IntStrat]
_ * _ (lens_scope) [notation, in models.IntStrat]
_ ∘ _ (lens_scope) [notation, in models.IntStrat]
_ ;; _ (lmap_scope) [notation, in models.Coherence]
_ * _ (mor_scope) [notation, in structures.Category]
_ @ _ (mor_scope) [notation, in structures.Category]
_ * _ (obj_scope) [notation, in structures.Category]
_ ^ _ (poset_scope) [notation, in lattices.LatticeProduct]
pi _ .. _ , _ (poset_scope) [notation, in lattices.LatticeProduct]
_ @ _ (rsq_scope) [notation, in models.IntStrat]
_ * _ (rsq_scope) [notation, in models.IntStrat]
_ + _ (rsq_scope) [notation, in models.IntStrat]
_ ;; _ (rsq_scope) [notation, in models.IntStrat]
_ ⊙ _ (rsq_scope) [notation, in models.IntStrat]
_ + _ (sig_scope) [notation, in models.Signature]
_ @ _ (strat_scope) [notation, in models.IntStrat]
_ * _ (strat_scope) [notation, in models.IntStrat]
_ + _ (strat_scope) [notation, in models.IntStrat]
_ ⊙ _ (strat_scope) [notation, in models.IntStrat]
_ --o _ (type_scope) [notation, in models.Coherence]
_ && _ [notation, in structures.Lattice]
_ || _ [notation, in structures.Lattice]
_ @ _ [notation, in examples.CAL]
_ / _ [notation, in examples.CAL]
_ # _ [notation, in examples.CAL]
_ <- _ ; _ [notation, in examples.CAL]
_ >>= _ [notation, in examples.CAL]
_ ~> _ [notation, in examples.CAL]
_ [= _ [notation, in models.DCPO]
_ [= _ [notation, in structures.Poset]
_ >= _ => _ [notation, in models.Signature]
_ <~> _ [notation, in models.IntStrat]
_ == _ [notation, in models.IntStrat]
_ ~>> _ [notation, in models.IntStrat]
_ <=> _ [notation, in models.IntStrat]
_ ->> _ [notation, in models.IntStrat]
_ :: _ [notation, in models.IntStrat]
inf { _ : _ | _ } , _ [notation, in structures.Lattice]
inf { _ | _ } , _ [notation, in structures.Lattice]
inf _ .. _ , _ [notation, in structures.Lattice]
sup { _ : _ | _ } , _ [notation, in structures.Lattice]
sup { _ | _ } , _ [notation, in structures.Lattice]
sup _ .. _ , _ [notation, in structures.Lattice]
# _ [notation, in models.Signature]
( _ @) [notation, in structures.Category]
(@ _ ) [notation, in structures.Category]
(@) [notation, in structures.Category]
0 [notation, in structures.Effects]
Notation Index
A
_ ∘ _ (hom_scope) [in interfaces.FunctorCategory]_ ∘ _ (obj_scope) [in interfaces.FunctorCategory]
C
_ & _ (hom_scope) [in interfaces.MonoidalCategory]_ & _ (obj_scope) [in interfaces.MonoidalCategory]
_ && _ (hom_scope) [in interfaces.MonoidalCategory]
_ && _ (obj_scope) [in interfaces.MonoidalCategory]
_ @ _ (hom_scope) [in interfaces.Category]
_ ~~> _ (type_scope) [in interfaces.Category]
_ + _ (hom_scope) [in interfaces.MonoidalCategory]
_ + _ (obj_scope) [in interfaces.MonoidalCategory]
_ + _ (hom_scope) [in interfaces.MonoidalCategory]
_ + _ (obj_scope) [in interfaces.MonoidalCategory]
0 [in interfaces.MonoidalCategory]
L
_ * _ (spec_scope) [in models.LinCCAL]_ <- _ ; _ [in models.LinCCAL]
_ >>= _ [in models.LinCCAL]
_ * _ (hom_scope) [in models.LinCCAL]
_ * _ (obj_scope) [in models.LinCCAL]
_ + _ [in models.LinCCAL]
M
_ * _ (hom_scope) [in interfaces.MonoidalCategory]_ * _ (obj_scope) [in interfaces.MonoidalCategory]
_ * _ (hom_scope) [in interfaces.MonoidalCategory]
_ * _ (obj_scope) [in interfaces.MonoidalCategory]
1 (obj_scope) [in interfaces.MonoidalCategory]
S
_ >= _ => _ (appl_scope) [in models.EffectSignatures]_ >= _ => _ (term_scope) [in models.EffectSignatures]
_ ⊳ _ (hom_scope) [in models.EffectSignatures]
_ ⊳ _ (obj_scope) [in models.EffectSignatures]
_ * _ (hom_scope) [in models.EffectSignatures]
_ * _ (obj_scope) [in models.EffectSignatures]
other
_ * _ (bijection_scope) [in models.IntStrat]_ ∘ _ (bijection_scope) [in models.IntStrat]
_ ^ _ (cdlat_scope) [in lattices.LatticeProduct]
pi _ .. _ , _ (cdlat_scope) [in lattices.LatticeProduct]
! _ (clique_scope) [in models.Coherence]
_ * _ (clique_scope) [in models.Coherence]
[ _ , _ ] (clique_scope) [in models.Coherence]
{ _ , _ } (clique_scope) [in models.Coherence]
_ @ _ (clique_scope) [in models.Coherence]
! _ (coh_scope) [in models.Coherence]
_ ;; _ (coh_scope) [in models.Coherence]
1 (coh_scope) [in models.Coherence]
_ * _ (coh_scope) [in models.Coherence]
_ + _ (coh_scope) [in models.Coherence]
_ && _ (coh_scope) [in models.Coherence]
_ --o _ (coh_scope) [in models.Coherence]
_ @ _ (conv_scope) [in models.IntStrat]
_ * _ (conv_scope) [in models.IntStrat]
_ + _ (conv_scope) [in models.IntStrat]
_ ;; _ (conv_scope) [in models.IntStrat]
_ * _ (emor_scope) [in models.IntStrat]
_ + _ (emor_scope) [in models.IntStrat]
_ ∘ _ (emor_scope) [in models.IntStrat]
_ + _ (esig_scope) [in structures.Effects]
_ @ _ (esig_scope) [in models.IntStrat]
_ * _ (esig_scope) [in models.IntStrat]
1 (esig_scope) [in models.IntStrat]
0 (esig_scope) [in models.IntStrat]
_ + _ (esig_scope) [in models.IntStrat]
_ * _ (lens_scope) [in models.IntStrat]
_ ∘ _ (lens_scope) [in models.IntStrat]
_ ;; _ (lmap_scope) [in models.Coherence]
_ * _ (mor_scope) [in structures.Category]
_ @ _ (mor_scope) [in structures.Category]
_ * _ (obj_scope) [in structures.Category]
_ ^ _ (poset_scope) [in lattices.LatticeProduct]
pi _ .. _ , _ (poset_scope) [in lattices.LatticeProduct]
_ @ _ (rsq_scope) [in models.IntStrat]
_ * _ (rsq_scope) [in models.IntStrat]
_ + _ (rsq_scope) [in models.IntStrat]
_ ;; _ (rsq_scope) [in models.IntStrat]
_ ⊙ _ (rsq_scope) [in models.IntStrat]
_ + _ (sig_scope) [in models.Signature]
_ @ _ (strat_scope) [in models.IntStrat]
_ * _ (strat_scope) [in models.IntStrat]
_ + _ (strat_scope) [in models.IntStrat]
_ ⊙ _ (strat_scope) [in models.IntStrat]
_ --o _ (type_scope) [in models.Coherence]
_ && _ [in structures.Lattice]
_ || _ [in structures.Lattice]
_ @ _ [in examples.CAL]
_ / _ [in examples.CAL]
_ # _ [in examples.CAL]
_ <- _ ; _ [in examples.CAL]
_ >>= _ [in examples.CAL]
_ ~> _ [in examples.CAL]
_ [= _ [in models.DCPO]
_ [= _ [in structures.Poset]
_ >= _ => _ [in models.Signature]
_ <~> _ [in models.IntStrat]
_ == _ [in models.IntStrat]
_ ~>> _ [in models.IntStrat]
_ <=> _ [in models.IntStrat]
_ ->> _ [in models.IntStrat]
_ :: _ [in models.IntStrat]
inf { _ : _ | _ } , _ [in structures.Lattice]
inf { _ | _ } , _ [in structures.Lattice]
inf _ .. _ , _ [in structures.Lattice]
sup { _ : _ | _ } , _ [in structures.Lattice]
sup { _ | _ } , _ [in structures.Lattice]
sup _ .. _ , _ [in structures.Lattice]
# _ [in models.Signature]
( _ @) [in structures.Category]
(@ _ ) [in structures.Category]
(@) [in structures.Category]
0 [in structures.Effects]
Module Index
A
AddEndofunctors [in interfaces.FunctorCategory]AddEndofunctors.End [in interfaces.FunctorCategory]
AddEndofunctors.EndNotations [in interfaces.FunctorCategory]
AddOp [in interfaces.Category]
AddOp.Op [in interfaces.Category]
B
Bifunctor [in interfaces.Functor]BifunctorDefinition [in interfaces.Functor]
BifunctorTheory [in interfaces.Functor]
BifunctorTheory.PC [in interfaces.Functor]
BifunctorTheory.PF [in interfaces.Functor]
C
Cartesian [in interfaces.MonoidalCategory]CartesianCategory [in interfaces.MonoidalCategory]
CartesianDefinition [in interfaces.MonoidalCategory]
CartesianDefinition.Prod [in interfaces.MonoidalCategory]
CartesianFromProducts [in interfaces.Limits]
CartesianFromProducts.Prod [in interfaces.Limits]
CartesianStructure [in interfaces.MonoidalCategory]
CartesianStructureDefinition [in interfaces.MonoidalCategory]
CartesianStructureFromProducts [in interfaces.Limits]
CartesianStructureLimit [in interfaces.Limits]
CartesianStructureTheory [in interfaces.MonoidalCategory]
CartesianTheory [in interfaces.MonoidalCategory]
Category [in interfaces.Category]
CategoryDefinition [in interfaces.Category]
CategoryTheory [in interfaces.Category]
CategoryWithEndofunctors [in interfaces.FunctorCategory]
CategoryWithOp [in interfaces.Category]
CDL [in lattices.FCD]
Cocartesian [in interfaces.MonoidalCategory]
CocartesianCategory [in interfaces.MonoidalCategory]
CocartesianDefinition [in interfaces.MonoidalCategory]
CocartesianDefinition.Plus [in interfaces.MonoidalCategory]
CocartesianStructure [in interfaces.MonoidalCategory]
CocartesianStructureDefinition [in interfaces.MonoidalCategory]
CocartesianStructureTheory [in interfaces.MonoidalCategory]
CocartesianTheory [in interfaces.MonoidalCategory]
Colimits [in interfaces.Limits]
ConcreteCategory [in interfaces.ConcreteCategory]
ConcreteCategoryDefinition [in interfaces.ConcreteCategory]
ConcreteCategoryTheory [in interfaces.ConcreteCategory]
Coproducts [in interfaces.Limits]
CoproductsDefinition [in interfaces.Limits]
CoproductsTheory [in interfaces.Limits]
cSET [in interfaces.ConcreteCategory]
D
DCPO [in models.DCPO]Downset [in lattices.Downset]
D2 [in interfaces.Limits]
E
EndofunctorCategory [in interfaces.FunctorCategory]EndofunctorComposition [in interfaces.FunctorCategory]
EndofunctorComposition.Tens [in interfaces.FunctorCategory]
Enriched [in interfaces.ConcreteCategory]
F
Faithful [in interfaces.Functor]FaithfulFunctor [in interfaces.Functor]
FCD [in lattices.FCD]
FCDSpec [in lattices.FCD]
Full [in interfaces.Functor]
FullAndFaithfulFunctor [in interfaces.Functor]
FullFunctor [in interfaces.Functor]
Functor [in interfaces.Functor]
FunctorCategory [in interfaces.FunctorCategory]
FunctorCategoryInstance [in interfaces.FunctorCategory]
FunctorComposition [in interfaces.FunctorCategory]
FunctorDefinition [in interfaces.Functor]
FunctorMonoidal [in interfaces.MonoidalCategory]
FunctorTheory [in interfaces.Functor]
I
Inf [in lattices.Upset]ISpec [in models.IntSpec]
J
JoinMeetDense [in lattices.FCD]L
LatticeCategory [in structures.Completion]LatticeCompletion [in structures.Completion]
LatticeCompletionDefs [in structures.Completion]
LatticeCompletionSpec [in structures.Completion]
Lazy [in lattices.AdjoinBot]
LBot [in lattices.AdjoinBot]
Limits [in interfaces.Limits]
LimitsPreliminaries [in interfaces.Limits]
LimitsPreliminaries.Diagram [in interfaces.Limits]
LinCCAL [in models.LinCCAL]
LinCCALBase [in models.LinCCAL]
LinCCALBase.Spec [in models.LinCCAL]
LinCCALBase.TMap [in models.LinCCAL]
LinCCALExample [in models.LinCCAL]
LinCCALTens [in models.LinCCAL]
LinCCALTensSpec [in models.LinCCAL]
LinCCALTens.Tens [in models.LinCCAL]
M
Monads [in interfaces.FunctorCategory]Monoidal [in interfaces.MonoidalCategory]
MonoidalCategory [in interfaces.MonoidalCategory]
MonoidalCategory [in interfaces.FunctorCategory]
MonoidalClosureDefinition [in interfaces.MonoidalCategory]
MonoidalClosureTheory [in interfaces.MonoidalCategory]
MonoidalDefinition [in interfaces.MonoidalCategory]
MonoidalDefinition.Tens [in interfaces.MonoidalCategory]
MonoidalFunctor [in interfaces.MonoidalCategory]
MonoidalStructure [in interfaces.MonoidalCategory]
MonoidalStructureDefinition [in interfaces.MonoidalCategory]
MonoidalStructureTheory [in interfaces.MonoidalCategory]
MonoidalTheory [in interfaces.MonoidalCategory]
Monoids [in interfaces.FunctorCategory]
O
One [in interfaces.Category]OppositeCategory [in interfaces.Category]
P
Poset [in models.DCPO]PreservesProducts [in interfaces.Limits]
Prod [in interfaces.Category]
Products [in interfaces.Limits]
ProductsDefinition [in interfaces.Limits]
ProductsTheory [in interfaces.Limits]
R
Reg [in models.EffectSignatures]RegBase [in models.EffectSignatures]
RegPlus [in models.EffectSignatures]
RegPlusReq [in models.EffectSignatures]
RegPlus.Plus [in models.EffectSignatures]
RegSpec [in models.EffectSignatures]
S
SET [in models.Sets]SET [in interfaces.Category]
SetBase [in models.Sets]
SetBaseSpec [in models.Sets]
SetMonoidalStructures [in models.Sets]
SetMonoidalStructures.Exp [in models.Sets]
SetMonoidalStructures.Prod [in models.Sets]
SetSpec [in models.Sets]
Sig [in models.EffectSignatures]
SigBase [in models.EffectSignatures]
SigComp [in models.EffectSignatures]
SigComp.Comp [in models.EffectSignatures]
SigEnd [in models.EffectSignatures]
SigMnd [in models.EffectSignatures]
SigPlus [in models.EffectSignatures]
SigPlusReq [in models.EffectSignatures]
SigPlus.Plus [in models.EffectSignatures]
SigReg [in models.EffectSignatures]
SigSpec [in models.EffectSignatures]
SigTens [in models.EffectSignatures]
SigTensReq [in models.EffectSignatures]
SigTens.Tens [in models.EffectSignatures]
SMnd [in models.Sets]
Sup [in lattices.Downset]
SymmetricMonoidal [in interfaces.MonoidalCategory]
SymmetricMonoidalCategory [in interfaces.MonoidalCategory]
SymmetricMonoidalDefinition [in interfaces.MonoidalCategory]
SymmetricMonoidalDefinition.Tens [in interfaces.MonoidalCategory]
SymmetricMonoidalStructure [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory [in interfaces.MonoidalCategory]
SymmetricMonoidalTheory [in interfaces.MonoidalCategory]
T
Two [in interfaces.Category]U
Upset [in lattices.Upset]V
VCOMP_NOT_ASSOC [in models.IntStrat]Z
Zero [in interfaces.Category]Library Index
A
AdjoinBotC
CALCategory
Category
Coherence
Completion
ConcreteCategory
D
DCPODownset
E
EffectsEffectSignatures
F
FCDFunctor
FunctorCategory
I
IntSpecIntStrat
L
LatticeLatticeProduct
Limits
LinCCAL
M
MonadMonoidalCategory
P
PosetS
SetsSignature
U
UpsetLemma Index
A
all_eq_none [in models.IntStrat]all_eq_some [in models.IntStrat]
amap_compose [in models.Signature]
amap_id [in models.Signature]
app_coh [in models.Coherence]
assert_r [in examples.CAL]
assert_l [in examples.CAL]
assert_true [in examples.CAL]
B
basis_hmap [in models.Signature]bcomp_bcomp [in models.IntStrat]
bcomp_bid_r [in models.IntStrat]
bcomp_bid_l [in models.IntStrat]
BifunctorTheory.PF.fmap_compose [in interfaces.Functor]
BifunctorTheory.PF.fmap_id [in interfaces.Functor]
bij_lens_bcomp [in models.IntStrat]
bij_eq_ext [in models.IntStrat]
bot_lb [in structures.Lattice]
bot_ref [in models.Coherence]
bq_rb_correct [in examples.CAL]
C
CartesianStructureFromProducts.pair_pi_compose [in interfaces.Limits]CartesianStructureFromProducts.p1_pair [in interfaces.Limits]
CartesianStructureFromProducts.p2_pair [in interfaces.Limits]
CartesianStructureFromProducts.ter_uni [in interfaces.Limits]
CartesianStructureTheory.assoc_coh [in interfaces.MonoidalCategory]
CartesianStructureTheory.assoc_nat [in interfaces.MonoidalCategory]
CartesianStructureTheory.fmap_compose [in interfaces.MonoidalCategory]
CartesianStructureTheory.fmap_id [in interfaces.MonoidalCategory]
CartesianStructureTheory.lunit_nat [in interfaces.MonoidalCategory]
CartesianStructureTheory.pair_compose [in interfaces.MonoidalCategory]
CartesianStructureTheory.pair_pi [in interfaces.MonoidalCategory]
CartesianStructureTheory.pair_uni [in interfaces.MonoidalCategory]
CartesianStructureTheory.p1_pair_rewrite [in interfaces.MonoidalCategory]
CartesianStructureTheory.p2_pair_rewrite [in interfaces.MonoidalCategory]
CartesianStructureTheory.runit_swap [in interfaces.MonoidalCategory]
CartesianStructureTheory.runit_nat [in interfaces.MonoidalCategory]
CartesianStructureTheory.swap_swap [in interfaces.MonoidalCategory]
CartesianStructureTheory.swap_assoc [in interfaces.MonoidalCategory]
CartesianStructureTheory.swap_nat [in interfaces.MonoidalCategory]
CartesianStructureTheory.unit_coh [in interfaces.MonoidalCategory]
CategoryTheory.bw_fw_rewrite [in interfaces.Category]
CategoryTheory.compose_bw_l_eq [in interfaces.Category]
CategoryTheory.compose_fw_l_eq [in interfaces.Category]
CategoryTheory.eq_fw_bw_r_2 [in interfaces.Category]
CategoryTheory.eq_fw_bw_l_2 [in interfaces.Category]
CategoryTheory.eq_fw_bw_r_1 [in interfaces.Category]
CategoryTheory.eq_fw_bw_l_1 [in interfaces.Category]
CategoryTheory.fw_bw_rewrite [in interfaces.Category]
CategoryTheory.iso_eq_fw_bw [in interfaces.Category]
CategoryTheory.iso_eq_bw [in interfaces.Category]
CategoryTheory.iso_eq_fw [in interfaces.Category]
CDL.compose_mor [in lattices.FCD]
CDL.id_mor [in lattices.FCD]
CocartesianStructureTheory.assoc_coh [in interfaces.MonoidalCategory]
CocartesianStructureTheory.assoc_nat [in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_compose [in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_iota [in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_uni [in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_i2_rewrite [in interfaces.MonoidalCategory]
CocartesianStructureTheory.copair_i1_rewrite [in interfaces.MonoidalCategory]
CocartesianStructureTheory.fmap_compose [in interfaces.MonoidalCategory]
CocartesianStructureTheory.fmap_id [in interfaces.MonoidalCategory]
CocartesianStructureTheory.lunit_nat [in interfaces.MonoidalCategory]
CocartesianStructureTheory.runit_swap [in interfaces.MonoidalCategory]
CocartesianStructureTheory.runit_nat [in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap_swap [in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap_assoc [in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap_nat [in interfaces.MonoidalCategory]
CocartesianStructureTheory.unit_coh [in interfaces.MonoidalCategory]
compose_fcomp_has [in models.IntStrat]
compose_assoc [in models.IntStrat]
compose_assoc_when [in models.IntStrat]
compose_id_r [in models.IntStrat]
compose_id_r_when [in models.IntStrat]
compose_id_has_r_lt [in models.IntStrat]
compose_id_has_r_gt [in models.IntStrat]
compose_id_l [in models.IntStrat]
compose_id_l_when [in models.IntStrat]
compose_id_has_l_lt [in models.IntStrat]
compose_id_has_l_gt [in models.IntStrat]
compose_next_la [in models.IntStrat]
compose_next_ra [in models.IntStrat]
compose_next_oa [in models.IntStrat]
compose_next_rq [in models.IntStrat]
compose_next_lq [in models.IntStrat]
compose_next_oq [in models.IntStrat]
comp_has_assoc_2 [in models.IntStrat]
comp_has_assoc_1 [in models.IntStrat]
comp_has_pref [in models.IntStrat]
ConcreteCategoryTheory.compose_assoc [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.compose_id_right [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.compose_id_left [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.meq [in interfaces.ConcreteCategory]
conv_has_forbid_cont [in models.IntStrat]
conv_has_forbid_allow [in models.IntStrat]
conv_has_cont_allow [in models.IntStrat]
copair_uniq [in models.Coherence]
copair_csi2 [in models.Coherence]
copair_csi1 [in models.Coherence]
CoproductsTheory.cotuple_uni [in interfaces.Limits]
CoproductsTheory.cotuple_iota_rewrite [in interfaces.Limits]
cspair_uniq [in models.Coherence]
cspair_csp2 [in models.Coherence]
cspair_csp1 [in models.Coherence]
cstens_compose [in models.Coherence]
cstens_id [in models.Coherence]
D
dag_ext_compose [in models.Coherence]dag_counit_ext [in models.Coherence]
dag_ext_counit [in models.Coherence]
dag_comult_comult [in models.Coherence]
dag_comult_app_inv [in models.Coherence]
dag_comult_app [in models.Coherence]
dag_counit_comult [in models.Coherence]
dag_comult_counit [in models.Coherence]
dag_comult_natural [in models.Coherence]
dag_lmaps_app_inv [in models.Coherence]
dag_lmaps_app [in models.Coherence]
dag_counit_natural [in models.Coherence]
dag_compose [in models.Coherence]
dag_id [in models.Coherence]
discard_uniq [in models.Coherence]
Downset.emb_join_prime [in lattices.Downset]
Downset.emb_join_dense [in lattices.Downset]
Downset.emb_mor [in lattices.Downset]
Downset.ext_unique [in lattices.Downset]
Downset.ext_ana [in lattices.Downset]
Downset.has_eq_ext [in lattices.Downset]
D2.compose_assoc [in interfaces.Limits]
D2.compose_id_right [in interfaces.Limits]
D2.compose_id_left [in interfaces.Limits]
E
ecomp_assoc [in models.IntStrat]ecomp_eid_r [in models.IntStrat]
ecomp_eid_l [in models.IntStrat]
emor_rc_ecomp [in models.IntStrat]
emor_rc_id [in models.IntStrat]
emor_strat_intro [in models.IntStrat]
emor_strat_intro_when [in models.IntStrat]
emor_strat_elim [in models.IntStrat]
emor_strat_elim_when [in models.IntStrat]
emor_strat_fcomp [in models.IntStrat]
emor_strat_fcomp_when [in models.IntStrat]
emor_strat_ecomp [in models.IntStrat]
emor_next [in models.IntStrat]
emor_next_answer [in models.IntStrat]
emor_next_question [in models.IntStrat]
encap_prod [in models.IntStrat]
EndofunctorComposition.Tens.assoc_coh [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.assoc_nat [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.lunit_nat [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.runit_nat [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.unit_coh [in interfaces.FunctorCategory]
estrat_ecomp_when [in models.IntStrat]
F
fassocr_fassoc [in models.IntStrat]fassoc_fassoc [in models.IntStrat]
fassoc_fassocr [in models.IntStrat]
FCD.emb_mor [in lattices.FCD]
FCD.ext_unique [in lattices.FCD]
FCD.ext_ana [in lattices.FCD]
FCD.join_meet_dense [in lattices.FCD]
FCD.meet_join_dense [in lattices.FCD]
fcomp_rsq [in models.IntStrat]
fcomp_rsp [in models.IntStrat]
fcomp_vcomp [in models.IntStrat]
fcomp_vid [in models.IntStrat]
fcomp_inf_r [in models.IntStrat]
fcomp_inf_l [in models.IntStrat]
fcomp_sup_r [in models.IntStrat]
fcomp_sup_l [in models.IntStrat]
fcomp_compose [in models.IntStrat]
fcomp_compose_when [in models.IntStrat]
fcomp_compose_has [in models.IntStrat]
fcomp_id [in models.IntStrat]
fcomp_next_pa_r [in models.IntStrat]
fcomp_next_pa_l [in models.IntStrat]
fcomp_next_oa_r [in models.IntStrat]
fcomp_next_oa_l [in models.IntStrat]
fcomp_next_pq_r [in models.IntStrat]
fcomp_next_pq_l [in models.IntStrat]
fcomp_next_oq_r [in models.IntStrat]
fcomp_next_oq_l [in models.IntStrat]
fcomp_has_closed [in models.IntStrat]
fcomp_ecomp [in models.IntStrat]
fcomp_eid [in models.IntStrat]
fdrop_uniq [in models.IntStrat]
ffst_fdup [in models.IntStrat]
ffst_fdrop [in models.IntStrat]
finf_glb [in structures.Lattice]
finf_at [in structures.Lattice]
finf_lb [in structures.Lattice]
flur_flu [in models.IntStrat]
flu_fassoc [in models.IntStrat]
flu_flur [in models.IntStrat]
fpair_expand [in models.IntStrat]
fpair_uniq [in models.IntStrat]
frur_fru [in models.IntStrat]
fru_frur [in models.IntStrat]
fsnd_fdup [in models.IntStrat]
fsnd_fdrop [in models.IntStrat]
fsup_lub [in structures.Lattice]
fsup_at [in structures.Lattice]
fsup_ub [in structures.Lattice]
fswap_fswap [in models.IntStrat]
fswap_assoc [in models.IntStrat]
fswap_unit [in models.IntStrat]
FunctorCategory.compose_assoc [in interfaces.FunctorCategory]
FunctorCategory.compose_id_right [in interfaces.FunctorCategory]
FunctorCategory.compose_id_left [in interfaces.FunctorCategory]
FunctorCategory.meq [in interfaces.FunctorCategory]
FunctorCategory.natural_rewrite [in interfaces.FunctorCategory]
FunctorComposition.fmap_compose [in interfaces.FunctorCategory]
FunctorComposition.fmap_id [in interfaces.FunctorCategory]
H
hmap_compose [in models.Signature]hmap_id [in models.Signature]
hmap_basis [in models.Signature]
hmap_natural [in models.Signature]
I
id_next [in models.IntStrat]imap_compose [in models.Coherence]
imap_id [in models.Coherence]
im_compose [in models.DCPO]
im_id [in models.DCPO]
inf_sup [in structures.Lattice]
inf_iff [in structures.Lattice]
inf_at [in structures.Lattice]
Inf.compose_mor [in lattices.Upset]
Inf.id_mor [in lattices.Upset]
Inf.mor_ref [in lattices.Upset]
Inf.mor_meet [in lattices.Upset]
inv_pswap [in models.IntStrat]
inv_r [in models.IntStrat]
inv_l [in models.IntStrat]
inv_invol [in models.IntStrat]
ISpec.apply_assoc [in models.IntSpec]
ISpec.apply_int_l [in models.IntSpec]
ISpec.apply_int_r [in models.IntSpec]
ISpec.apply_bind [in models.IntSpec]
ISpec.apply_ret [in models.IntSpec]
ISpec.bind_bind [in models.IntSpec]
ISpec.bind_ret_l [in models.IntSpec]
ISpec.bind_ret_r [in models.IntSpec]
ISpec.compose_assoc [in models.IntSpec]
ISpec.compose_int_r [in models.IntSpec]
ISpec.compose_int_l [in models.IntSpec]
ISpec.pbind_ret_l [in models.IntSpec]
J
join_idemp [in structures.Lattice]join_comm [in structures.Lattice]
join_meet_l [in structures.Lattice]
join_top_l [in structures.Lattice]
join_bot_l [in structures.Lattice]
join_r [in structures.Lattice]
join_l [in structures.Lattice]
join_lub [in structures.Lattice]
join_ub_r [in structures.Lattice]
join_ub_l [in structures.Lattice]
L
LatticeCompletionDefs.ext_ext [in structures.Completion]LatticeCompletionDefs.ext_emb [in structures.Completion]
Lazy.compose_mor [in lattices.AdjoinBot]
Lazy.id_mor [in lattices.AdjoinBot]
LBot.cases [in lattices.AdjoinBot]
LBot.ext_unique [in lattices.AdjoinBot]
LBot.ext_ana [in lattices.AdjoinBot]
LBot.ext_bot [in lattices.AdjoinBot]
LBot.is_unique [in lattices.AdjoinBot]
LBot.opt_eq [in lattices.AdjoinBot]
LBot.proj_is [in lattices.AdjoinBot]
LBot.sup_cases [in lattices.AdjoinBot]
LBot.sup_inf_of_cd [in lattices.AdjoinBot]
lcj_elim [in models.IntStrat]
lcj_elim_when [in models.IntStrat]
lcj_intro [in models.IntStrat]
lcj_intro_when [in models.IntStrat]
lcomp_lcomp [in models.IntStrat]
lcomp_lid_r [in models.IntStrat]
lcomp_lid_l [in models.IntStrat]
lcp_elim [in models.IntStrat]
lcp_elim_when [in models.IntStrat]
lcp_intro [in models.IntStrat]
lcp_intro_when [in models.IntStrat]
lens_strat_ref [in models.IntStrat]
lens_strat_next_pa [in models.IntStrat]
lens_strat_next_oa [in models.IntStrat]
lens_strat_next_pq [in models.IntStrat]
lens_strat_next_oq [in models.IntStrat]
le_directed [in models.DCPO]
LimitsPreliminaries.cone_mor_eq [in interfaces.Limits]
lim_sup [in models.Coherence]
LinCCALBase.compose_assoc [in models.LinCCAL]
LinCCALBase.compose_id_right [in models.LinCCAL]
LinCCALBase.compose_id_left [in models.LinCCAL]
LinCCALBase.comp_cal [in models.LinCCAL]
LinCCALBase.comp_ci [in models.LinCCAL]
LinCCALBase.comp_run [in models.LinCCAL]
LinCCALBase.comp_run_r [in models.LinCCAL]
LinCCALBase.comp_specified_sufficient [in models.LinCCAL]
LinCCALBase.comp_tmap_commit_r [in models.LinCCAL]
LinCCALBase.comp_tmap_commit_l [in models.LinCCAL]
LinCCALBase.comp_tmap_return_r [in models.LinCCAL]
LinCCALBase.comp_tmap_action_r [in models.LinCCAL]
LinCCALBase.comp_tmap_invoke_r [in models.LinCCAL]
LinCCALBase.comp_tmap_return_l [in models.LinCCAL]
LinCCALBase.comp_tmap_action_l [in models.LinCCAL]
LinCCALBase.comp_tmap_invoke_l [in models.LinCCAL]
LinCCALBase.comp_tmap_specified_r [in models.LinCCAL]
LinCCALBase.comp_tmap_specified_l [in models.LinCCAL]
LinCCALBase.comp_tmap_convert [in models.LinCCAL]
LinCCALBase.comp_threadstate_o [in models.LinCCAL]
LinCCALBase.comp_threadstate_valid [in models.LinCCAL]
LinCCALBase.correctness_invariant_sound [in models.LinCCAL]
LinCCALBase.correct_ci [in models.LinCCAL]
LinCCALBase.id_cal [in models.LinCCAL]
LinCCALBase.id_state_ci [in models.LinCCAL]
LinCCALBase.lsteps_ind [in models.LinCCAL]
LinCCALBase.meq [in models.LinCCAL]
LinCCALBase.reachable_steps [in models.LinCCAL]
LinCCALBase.reachable_step [in models.LinCCAL]
LinCCALBase.reachable_base [in models.LinCCAL]
LinCCALExample.fai_threadstate_convert [in models.LinCCAL]
LinCCALTens.Tens.assoc_coh [in models.LinCCAL]
LinCCALTens.Tens.assoc_nat [in models.LinCCAL]
LinCCALTens.Tens.fmap_compose [in models.LinCCAL]
LinCCALTens.Tens.fmap_id [in models.LinCCAL]
LinCCALTens.Tens.fmap_ci [in models.LinCCAL]
LinCCALTens.Tens.fmap_lsteps_r [in models.LinCCAL]
LinCCALTens.Tens.fmap_lsteps_l [in models.LinCCAL]
LinCCALTens.Tens.fmap_tmap_specified_r [in models.LinCCAL]
LinCCALTens.Tens.fmap_tmap_specified_l [in models.LinCCAL]
LinCCALTens.Tens.inj_somets2 [in models.LinCCAL]
LinCCALTens.Tens.lunit_nat [in models.LinCCAL]
LinCCALTens.Tens.runit_swap [in models.LinCCAL]
LinCCALTens.Tens.runit_nat [in models.LinCCAL]
LinCCALTens.Tens.swap_swap [in models.LinCCAL]
LinCCALTens.Tens.swap_assoc [in models.LinCCAL]
LinCCALTens.Tens.swap_nat [in models.LinCCAL]
LinCCALTens.Tens.unit_coh [in models.LinCCAL]
lmap_apply_compose [in models.Coherence]
lmap_apply_id [in models.Coherence]
lmap_compose_assoc [in models.Coherence]
lmap_compose_id_right [in models.Coherence]
lmap_compose_id_left [in models.Coherence]
lmap_ext [in models.Coherence]
lmap_det [in models.Coherence]
lmap_coh [in models.Coherence]
M
meet_idemp [in structures.Lattice]meet_comm [in structures.Lattice]
meet_r [in structures.Lattice]
meet_l [in structures.Lattice]
meet_glb [in structures.Lattice]
meet_lb_r [in structures.Lattice]
meet_lb_l [in structures.Lattice]
MonoidalClosureTheory.curry_natural [in interfaces.MonoidalCategory]
MonoidalStructureTheory.assoc_coh_bw [in interfaces.MonoidalCategory]
MonoidalStructureTheory.assoc_nat_bw [in interfaces.MonoidalCategory]
MonoidalStructureTheory.lunit_nat_bw [in interfaces.MonoidalCategory]
MonoidalStructureTheory.runit_nat_bw [in interfaces.MonoidalCategory]
MonoidalStructureTheory.unit_coh_bw [in interfaces.MonoidalCategory]
Monoids.compose_assoc [in interfaces.FunctorCategory]
Monoids.compose_id_right [in interfaces.FunctorCategory]
Monoids.compose_id_left [in interfaces.FunctorCategory]
Monoids.map_mu_rewrite [in interfaces.FunctorCategory]
Monoids.map_eta_rewrite [in interfaces.FunctorCategory]
Monoids.meq [in interfaces.FunctorCategory]
O
oa_eq_inv [in models.IntStrat]oext_uniq [in models.Coherence]
oext_oret [in models.Coherence]
omap_compose [in models.Coherence]
omap_id [in models.Coherence]
One.compose_assoc [in interfaces.Category]
One.compose_id_right [in interfaces.Category]
One.compose_id_left [in interfaces.Category]
OppositeCategory.compose_assoc [in interfaces.Category]
OppositeCategory.compose_id_right [in interfaces.Category]
OppositeCategory.compose_id_left [in interfaces.Category]
P
passoc_pswap [in models.IntStrat]passoc_passoc [in models.IntStrat]
pa_eq_inv [in models.IntStrat]
pcoh_inv_pa [in models.IntStrat]
pcoh_inv_pq [in models.IntStrat]
pcons_pa_inv [in models.IntStrat]
pcons_oa_inv [in models.IntStrat]
pcons_eq_inv_r [in models.IntStrat]
pcons_eq_inv_l [in models.IntStrat]
plu_pswap [in models.IntStrat]
plu_passoc [in models.IntStrat]
prefix_coh [in models.Coherence]
pref_refl [in models.IntStrat]
ProductsTheory.pi_tuple_rewrite [in interfaces.Limits]
ProductsTheory.tuple_uni [in interfaces.Limits]
prod_bij_bcomp [in models.IntStrat]
prod_bij_id [in models.IntStrat]
Prod.compose_assoc [in interfaces.Category]
Prod.compose_id_right [in interfaces.Category]
Prod.compose_id_left [in interfaces.Category]
pswap_pswap [in models.IntStrat]
R
rcnext_lcj [in models.IntStrat]rcnext_lcp [in models.IntStrat]
rcnext_tconv [in models.IntStrat]
rcnext_fcomp_r [in models.IntStrat]
rcnext_fcomp_l [in models.IntStrat]
rcnext_emor [in models.IntStrat]
rcnext_vcomp_at [in models.IntStrat]
rcnext_vid [in models.IntStrat]
rcnext_sup [in models.IntStrat]
rcnext_inf [in models.IntStrat]
ref_meet [in structures.Lattice]
ref_join [in structures.Lattice]
RegBase.compose_assoc [in models.EffectSignatures]
RegBase.compose_id_right [in models.EffectSignatures]
RegBase.compose_id_left [in models.EffectSignatures]
RegBase.transform_compose [in models.EffectSignatures]
RegBase.transform_id [in models.EffectSignatures]
RegPlus.Plus.copair_iota_compose [in models.EffectSignatures]
RegPlus.Plus.copair_i2 [in models.EffectSignatures]
RegPlus.Plus.copair_i1 [in models.EffectSignatures]
RegPlus.Plus.ini_uni [in models.EffectSignatures]
retract [in models.IntStrat]
rsp_vcomp [in models.IntStrat]
rsp_comp [in models.IntStrat]
rsp_inf [in models.IntStrat]
rsp_sup [in models.IntStrat]
rsp_sup_cases [in models.IntStrat]
rsp_suspended_inv_nil [in models.IntStrat]
rsp_ready_inv_nil [in models.IntStrat]
rsq_vcomp [in models.IntStrat]
rsq_vcomp_when [in models.IntStrat]
rsq_comp [in models.IntStrat]
rsq_comp_when [in models.IntStrat]
rsq_sup [in models.IntStrat]
rsq_next_pa [in models.IntStrat]
rsq_next_oa [in models.IntStrat]
rsq_next_pq [in models.IntStrat]
rsq_next_oq [in models.IntStrat]
S
scomp_vcomp [in models.IntStrat]scomp_vid [in models.IntStrat]
scomp_compose [in models.IntStrat]
scomp_compose_when_2 [in models.IntStrat]
scomp_compose_when_1 [in models.IntStrat]
scomp_id [in models.IntStrat]
scomp_id_when [in models.IntStrat]
scomp_rsq [in models.IntStrat]
scons_next_adj [in models.IntStrat]
sc_dsup [in models.DCPO]
SetBase.compose_assoc [in models.Sets]
SetBase.compose_id_right [in models.Sets]
SetBase.compose_id_left [in models.Sets]
SetBase.natural [in models.Sets]
SetMonoidalStructures.Exp.curry_natural_r [in models.Sets]
SetMonoidalStructures.Exp.curry_natural_l [in models.Sets]
SetMonoidalStructures.Exp.curry_uncurry [in models.Sets]
SetMonoidalStructures.Exp.fmap_compose [in models.Sets]
SetMonoidalStructures.Exp.fmap_id [in models.Sets]
SetMonoidalStructures.Exp.uncurry_curry [in models.Sets]
SetMonoidalStructures.Prod.pair_pi_compose [in models.Sets]
SetMonoidalStructures.Prod.p1_pair [in models.Sets]
SetMonoidalStructures.Prod.p2_pair [in models.Sets]
SetMonoidalStructures.Prod.ter_uni [in models.Sets]
SET.compose_assoc [in interfaces.Category]
SET.compose_id_right [in interfaces.Category]
SET.compose_id_left [in interfaces.Category]
SigBase.amap_compose [in models.EffectSignatures]
SigBase.amap_id [in models.EffectSignatures]
SigBase.compose_assoc [in models.EffectSignatures]
SigBase.compose_id_right [in models.EffectSignatures]
SigBase.compose_id_left [in models.EffectSignatures]
SigBase.cotuple_iota [in models.EffectSignatures]
SigBase.hmap_compose [in models.EffectSignatures]
SigBase.hmap_id [in models.EffectSignatures]
SigBase.hmap_natural [in models.EffectSignatures]
SigBase.iota_cotuple [in models.EffectSignatures]
SigBase.pi_tuple [in models.EffectSignatures]
SigBase.subst_expand [in models.EffectSignatures]
SigBase.subst_tmap [in models.EffectSignatures]
SigBase.subst_subst [in models.EffectSignatures]
SigBase.subst_cons [in models.EffectSignatures]
SigBase.subst_var_r [in models.EffectSignatures]
SigBase.subst_var_l [in models.EffectSignatures]
SigBase.tmap_tmul [in models.EffectSignatures]
SigBase.tmap_cons [in models.EffectSignatures]
SigBase.tmap_var [in models.EffectSignatures]
SigBase.tmap_compose [in models.EffectSignatures]
SigBase.tmap_id [in models.EffectSignatures]
SigBase.tmul_var_r [in models.EffectSignatures]
SigBase.tmul_var_l [in models.EffectSignatures]
SigBase.tmul_natural [in models.EffectSignatures]
SigBase.transform_compose [in models.EffectSignatures]
SigBase.transform_id [in models.EffectSignatures]
SigBase.tuple_pi [in models.EffectSignatures]
sigcomp_assoc [in models.Signature]
sigcomp_id_r [in models.Signature]
sigcomp_id_l [in models.Signature]
SigComp.Comp.aeq [in models.EffectSignatures]
SigComp.Comp.aeq' [in models.EffectSignatures]
SigComp.Comp.assoc_coh [in models.EffectSignatures]
SigComp.Comp.assoc_nat [in models.EffectSignatures]
SigComp.Comp.fmap_compose [in models.EffectSignatures]
SigComp.Comp.fmap_id [in models.EffectSignatures]
SigComp.Comp.lunit_nat [in models.EffectSignatures]
SigComp.Comp.runit_nat [in models.EffectSignatures]
SigComp.Comp.unit_coh [in models.EffectSignatures]
SigEnd.faithful [in models.EffectSignatures]
SigEnd.fmap_compose [in models.EffectSignatures]
SigEnd.fmap_id [in models.EffectSignatures]
SigEnd.full [in models.EffectSignatures]
SigMnd.faithful [in models.EffectSignatures]
SigMnd.fmap_compose [in models.EffectSignatures]
SigMnd.fmap_id [in models.EffectSignatures]
SigMnd.full [in models.EffectSignatures]
SigMnd.map_cons [in models.EffectSignatures]
SigMnd.map_var [in models.EffectSignatures]
SigPlus.Plus.copair_iota_compose [in models.EffectSignatures]
SigPlus.Plus.copair_i2 [in models.EffectSignatures]
SigPlus.Plus.copair_i1 [in models.EffectSignatures]
SigPlus.Plus.ini_uni [in models.EffectSignatures]
SigReg.faithful [in models.EffectSignatures]
SigReg.fmap_compose [in models.EffectSignatures]
SigReg.fmap_id [in models.EffectSignatures]
SigTens.Tens.assoc_coh [in models.EffectSignatures]
SigTens.Tens.assoc_nat [in models.EffectSignatures]
SigTens.Tens.fmap_compose [in models.EffectSignatures]
SigTens.Tens.fmap_id [in models.EffectSignatures]
SigTens.Tens.lunit_nat [in models.EffectSignatures]
SigTens.Tens.runit_swap [in models.EffectSignatures]
SigTens.Tens.runit_nat [in models.EffectSignatures]
SigTens.Tens.swap_swap [in models.EffectSignatures]
SigTens.Tens.swap_assoc [in models.EffectSignatures]
SigTens.Tens.swap_nat [in models.EffectSignatures]
SigTens.Tens.unit_coh [in models.EffectSignatures]
sigtup_uniq [in models.Signature]
sigtup_inr [in models.Signature]
sigtup_inl [in models.Signature]
slice_length [in examples.CAL]
srel_push_pull [in examples.CAL]
srun_int [in examples.CAL]
srun_bind [in examples.CAL]
srun_slift [in examples.CAL]
srur_natural [in models.IntStrat]
sru_natural [in models.IntStrat]
sru_natural_has_2 [in models.IntStrat]
sru_natural_has_1 [in models.IntStrat]
strat_has_any_pnil_suspended [in models.IntStrat]
strat_has_any_pnil_ready [in models.IntStrat]
strat_closed [in models.IntStrat]
suffix_coh [in models.Coherence]
sup_iff [in structures.Lattice]
sup_at [in structures.Lattice]
sup_unique [in models.DCPO]
Sup.compose_mor [in lattices.Downset]
Sup.id_mor [in lattices.Downset]
Sup.mor_bot [in lattices.Downset]
Sup.mor_ref [in lattices.Downset]
Sup.mor_join [in lattices.Downset]
SymmetricMonoidalStructureTheory.lunit_swap_bw [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.lunit_swap [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.runit_swap_bw [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureTheory.swap_assoc_bw [in interfaces.MonoidalCategory]
T
tassocr_tassoc [in models.IntStrat]tassoc_tswap [in models.IntStrat]
tassoc_tassoc [in models.IntStrat]
tassoc_tassocr [in models.IntStrat]
tconv_vid [in models.IntStrat]
tconv_vcomp [in models.IntStrat]
tconv_vcomp_at [in models.IntStrat]
tconv_inf_r [in models.IntStrat]
tconv_inf_l [in models.IntStrat]
tconv_sup [in models.IntStrat]
tconv_sup_r [in models.IntStrat]
tconv_sup_l [in models.IntStrat]
tens_compose [in models.IntStrat]
tens_eid [in models.IntStrat]
tlur_tlu [in models.IntStrat]
tlu_tswap [in models.IntStrat]
tlu_tassoc [in models.IntStrat]
tlu_tlur [in models.IntStrat]
tmap_compose [in models.Sets]
tmap_id [in models.Sets]
top_ub [in structures.Lattice]
trsp [in models.IntStrat]
trsq [in models.IntStrat]
trur_tru [in models.IntStrat]
tru_trur [in models.IntStrat]
tstrat_next_pa [in models.IntStrat]
tstrat_next_oa [in models.IntStrat]
tstrat_next_pq [in models.IntStrat]
tstrat_next_oq [in models.IntStrat]
tswap_tswap [in models.IntStrat]
Two.compose_assoc [in interfaces.Category]
Two.compose_id_right [in interfaces.Category]
Two.compose_id_left [in interfaces.Category]
U
Upset.emb_mor [in lattices.Upset]Upset.ext_unique [in lattices.Upset]
Upset.ext_ana [in lattices.Upset]
V
VCOMP_NOT_ASSOC.vcomp_not_assoc [in models.IntStrat]vcomp_vid_r [in models.IntStrat]
vcomp_vid_l [in models.IntStrat]
vcomp_expand [in models.IntStrat]
Z
Zero.compose_assoc [in interfaces.Category]Zero.compose_id_right [in interfaces.Category]
Zero.compose_id_left [in interfaces.Category]
Constructor Index
A
apply [in models.Signature]B
bq_rb_intro [in examples.CAL]C
ccpos_suspended [in models.IntStrat]ccpos_right [in models.IntStrat]
ccpos_mid [in models.IntStrat]
ccpos_left [in models.IntStrat]
ccpos_ready [in models.IntStrat]
CDL.mor [in lattices.FCD]
cepos_suspended [in models.IntStrat]
cepos_ready [in models.IntStrat]
comp_la [in models.IntStrat]
comp_ra [in models.IntStrat]
comp_oa [in models.IntStrat]
comp_suspended [in models.IntStrat]
comp_rq [in models.IntStrat]
comp_lq [in models.IntStrat]
comp_oq [in models.IntStrat]
comp_ready [in models.IntStrat]
ConcreteCategoryTheory.mkm [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.mkt [in interfaces.ConcreteCategory]
cons [in models.Sets]
cons_coh [in models.Coherence]
cpos_suspended [in models.IntStrat]
cpos_right [in models.IntStrat]
cpos_left [in models.IntStrat]
cpos_ready [in models.IntStrat]
D
dag_comult_cons [in models.Coherence]dag_comult_nil [in models.Coherence]
dag_counit_intro [in models.Coherence]
dag_lmaps_cons [in models.Coherence]
dag_lmaps_nil [in models.Coherence]
deq [in examples.CAL]
deq [in models.Signature]
directed [in models.DCPO]
D2.id_def [in interfaces.Limits]
E
econs [in models.IntStrat]einl [in structures.Effects]
einr [in structures.Effects]
emor_rc_cont [in models.IntStrat]
emor_rc_forbid [in models.IntStrat]
emor_rc_allow [in models.IntStrat]
emor_answer [in models.IntStrat]
emor_suspended [in models.IntStrat]
emor_question [in models.IntStrat]
emor_ready [in models.IntStrat]
enq [in examples.CAL]
enq [in models.Signature]
eready [in models.IntStrat]
ese_suspended [in models.IntStrat]
ese_ready [in models.IntStrat]
esi_suspended [in models.IntStrat]
esi_ready [in models.IntStrat]
esuspended [in models.IntStrat]
F
fccpos_suspended_r [in models.IntStrat]fccpos_suspended_l [in models.IntStrat]
fccpos_right_r [in models.IntStrat]
fccpos_right_l [in models.IntStrat]
fccpos_left_r [in models.IntStrat]
fccpos_left_l [in models.IntStrat]
fccpos_ready [in models.IntStrat]
fcomp_pa_r [in models.IntStrat]
fcomp_pa_l [in models.IntStrat]
fcomp_oa_r [in models.IntStrat]
fcomp_oa_l [in models.IntStrat]
fcomp_suspended_r [in models.IntStrat]
fcomp_suspended_l [in models.IntStrat]
fcomp_pq_r [in models.IntStrat]
fcomp_pq_l [in models.IntStrat]
fcomp_oq_r [in models.IntStrat]
fcomp_oq_l [in models.IntStrat]
fcomp_ready [in models.IntStrat]
fcpos_suspended_r [in models.IntStrat]
fcpos_suspended_l [in models.IntStrat]
fcpos_running_r [in models.IntStrat]
fcpos_running_l [in models.IntStrat]
fcpos_ready [in models.IntStrat]
fcrs_suspended_r [in models.IntStrat]
fcrs_suspended_l [in models.IntStrat]
fcrs_running_r [in models.IntStrat]
fcrs_running_l [in models.IntStrat]
fcrs_ready [in models.IntStrat]
FunctorCategory.mknt [in interfaces.FunctorCategory]
G
get [in examples.CAL]get [in models.Signature]
getbit [in models.Sets]
I
im_intro [in models.DCPO]inc1 [in examples.CAL]
inc1 [in models.Signature]
inc2 [in examples.CAL]
inc2 [in models.Signature]
Inf.mor [in lattices.Upset]
inl_inr_coh [in models.Coherence]
inl_coh [in models.Coherence]
inr_inl_coh [in models.Coherence]
inr_coh [in models.Coherence]
ISpec.pcons [in models.IntSpec]
ISpec.pcons_ref [in models.IntSpec]
ISpec.pmove [in models.IntSpec]
ISpec.pmove_cons_ref [in models.IntSpec]
ISpec.pmove_ref [in models.IntSpec]
ISpec.pret [in models.IntSpec]
ISpec.pret_ref [in models.IntSpec]
L
Lazy.mor [in lattices.AdjoinBot]Lazy.mor_sup [in lattices.AdjoinBot]
LBot.mkopt [in lattices.AdjoinBot]
lcje_suspended [in models.IntStrat]
lcje_running [in models.IntStrat]
lcje_ready [in models.IntStrat]
lcji_suspended [in models.IntStrat]
lcji_running [in models.IntStrat]
lcji_ready [in models.IntStrat]
lcpe_suspended [in models.IntStrat]
lcpe_running [in models.IntStrat]
lcpe_ready [in models.IntStrat]
lcpi_suspended [in models.IntStrat]
lcpi_running [in models.IntStrat]
lcpi_ready [in models.IntStrat]
lens_pa [in models.IntStrat]
lens_oa [in models.IntStrat]
lens_suspended [in models.IntStrat]
lens_pq [in models.IntStrat]
lens_oq [in models.IntStrat]
lens_ready [in models.IntStrat]
LinCCALBase.comp_state_intro [in models.LinCCAL]
LinCCALBase.comp_running [in models.LinCCAL]
LinCCALBase.comp_ready [in models.LinCCAL]
LinCCALBase.cts_right [in models.LinCCAL]
LinCCALBase.cts_left [in models.LinCCAL]
LinCCALBase.cts_ready [in models.LinCCAL]
LinCCALBase.eaction [in models.LinCCAL]
LinCCALBase.einvoke [in models.LinCCAL]
LinCCALBase.ereturn [in models.LinCCAL]
LinCCALBase.id_state_intro [in models.LinCCAL]
LinCCALBase.id_returned [in models.LinCCAL]
LinCCALBase.id_invoked [in models.LinCCAL]
LinCCALBase.lcommit [in models.LinCCAL]
LinCCALBase.mkst [in models.LinCCAL]
LinCCALBase.mkts [in models.LinCCAL]
LinCCALBase.run_check_r_var [in models.LinCCAL]
LinCCALBase.run_check_r_cons [in models.LinCCAL]
LinCCALBase.run_check_l_var [in models.LinCCAL]
LinCCALBase.run_check_l_cons [in models.LinCCAL]
LinCCALBase.Spec.bot [in models.LinCCAL]
LinCCALBase.Spec.ret [in models.LinCCAL]
LinCCALBase.Spec.top [in models.LinCCAL]
LinCCALExample.acq [in models.LinCCAL]
LinCCALExample.fai [in models.LinCCAL]
LinCCALExample.fai_state_intro [in models.LinCCAL]
LinCCALExample.fai_ret [in models.LinCCAL]
LinCCALExample.fai_rel [in models.LinCCAL]
LinCCALExample.fai_set [in models.LinCCAL]
LinCCALExample.fai_get [in models.LinCCAL]
LinCCALExample.fai_acq [in models.LinCCAL]
LinCCALExample.fai_rdy [in models.LinCCAL]
LinCCALExample.get [in models.LinCCAL]
LinCCALExample.rel [in models.LinCCAL]
LinCCALExample.set [in models.LinCCAL]
LinCCALTens.Tens.assoc_bw_state_intro [in models.LinCCAL]
LinCCALTens.Tens.assoc_fw_state_intro [in models.LinCCAL]
LinCCALTens.Tens.fmap_state_intro [in models.LinCCAL]
LinCCALTens.Tens.fmap_ts_right [in models.LinCCAL]
LinCCALTens.Tens.fmap_ts_left [in models.LinCCAL]
LinCCALTens.Tens.fmap_ts_none [in models.LinCCAL]
LinCCALTens.Tens.iso_returned [in models.LinCCAL]
LinCCALTens.Tens.iso_invoked [in models.LinCCAL]
LinCCALTens.Tens.lunit_bw_state_intro [in models.LinCCAL]
LinCCALTens.Tens.lunit_fw_state_intro [in models.LinCCAL]
LinCCALTens.Tens.runit_bw_state_intro [in models.LinCCAL]
LinCCALTens.Tens.runit_fw_state_intro [in models.LinCCAL]
LinCCALTens.Tens.swap_state_intro [in models.LinCCAL]
ln [in models.Coherence]
lneg_coh_intro [in models.Coherence]
lready [in models.IntStrat]
lready_eqv [in models.IntStrat]
lrunning [in models.IntStrat]
lrunning_eqv [in models.IntStrat]
lsuspended [in models.IntStrat]
lsuspended_eqv [in models.IntStrat]
N
nil_coh_r [in models.Coherence]nil_coh_l [in models.Coherence]
O
oa [in models.IntStrat]oq [in models.IntStrat]
P
pa [in models.IntStrat]pcons [in models.IntStrat]
pcons_pcoh_oa [in models.IntStrat]
pcons_pcoh_oq [in models.IntStrat]
pcons_pcoh [in models.IntStrat]
pcons_pref [in models.IntStrat]
pnil_suspended_pcoh_r [in models.IntStrat]
pnil_suspended_pcoh_l [in models.IntStrat]
pnil_ready_pcoh_r [in models.IntStrat]
pnil_ready_pcoh_l [in models.IntStrat]
pnil_suspended_pref [in models.IntStrat]
pnil_ready_pref [in models.IntStrat]
pnil_suspended [in models.IntStrat]
pnil_ready [in models.IntStrat]
pq [in models.IntStrat]
R
rcp_forbid_ref [in models.IntStrat]rcp_cont_forbid_ref [in models.IntStrat]
rcp_cont_ref [in models.IntStrat]
rcp_allow_forbid_ref [in models.IntStrat]
rcp_allow_cont_ref [in models.IntStrat]
rcp_allow_ref [in models.IntStrat]
rcp_cont [in models.IntStrat]
rcp_forbid [in models.IntStrat]
rcp_allow [in models.IntStrat]
ready [in models.IntStrat]
rsc_suspended [in models.IntStrat]
rsc_right [in models.IntStrat]
rsc_left [in models.IntStrat]
rsc_ready [in models.IntStrat]
rsp_pa [in models.IntStrat]
rsp_oa [in models.IntStrat]
rsp_suspended [in models.IntStrat]
rsp_pq [in models.IntStrat]
rsp_oq [in models.IntStrat]
rsp_ready [in models.IntStrat]
rsv_suspended [in models.IntStrat]
rsv_running [in models.IntStrat]
rsv_ready [in models.IntStrat]
rs_suspended [in models.IntStrat]
rs_running [in models.IntStrat]
rs_ready [in models.IntStrat]
running [in models.IntStrat]
S
scc_suspended [in models.IntStrat]scc_right [in models.IntStrat]
scc_left [in models.IntStrat]
scc_ready [in models.IntStrat]
sci_suspended [in models.IntStrat]
sci_ready [in models.IntStrat]
set [in examples.CAL]
set [in models.Signature]
SigBase.apply [in models.EffectSignatures]
SigBase.cons [in models.EffectSignatures]
SigBase.mkop [in models.EffectSignatures]
SigBase.mkops [in models.EffectSignatures]
SigBase.sig_esig_op [in models.EffectSignatures]
SigBase.var [in models.EffectSignatures]
SigComp.Comp.mkar [in models.EffectSignatures]
SigComp.Comp.mkop [in models.EffectSignatures]
srun_suspended [in models.IntStrat]
srun_running [in models.IntStrat]
srun_ready [in models.IntStrat]
st [in examples.CAL]
sum_inr_coh [in models.Coherence]
sum_inl_coh [in models.Coherence]
Sup.mor [in lattices.Downset]
suspended [in models.IntStrat]
T
tp_suspended [in models.IntStrat]tp_running [in models.IntStrat]
tp_ready [in models.IntStrat]
trs_suspended [in models.IntStrat]
trs_running [in models.IntStrat]
trs_ready [in models.IntStrat]
tstrat_has_pa [in models.IntStrat]
tstrat_has_oa [in models.IntStrat]
tstrat_has_suspended [in models.IntStrat]
tstrat_has_pq [in models.IntStrat]
tstrat_has_oq [in models.IntStrat]
tstrat_has_ready [in models.IntStrat]
Two.id_def [in interfaces.Category]
Two.int [in interfaces.Category]
V
var [in models.Sets]VCOMP_NOT_ASSOC.foo_cont [in models.IntStrat]
VCOMP_NOT_ASSOC.foo_r [in models.IntStrat]
VCOMP_NOT_ASSOC.foo_q [in models.IntStrat]
Axiom Index
B
BifunctorDefinition.fmap [in interfaces.Functor]BifunctorDefinition.fmap_compose [in interfaces.Functor]
BifunctorDefinition.fmap_id [in interfaces.Functor]
BifunctorDefinition.omap [in interfaces.Functor]
C
CartesianStructureDefinition.omap [in interfaces.MonoidalCategory]CartesianStructureDefinition.pair [in interfaces.MonoidalCategory]
CartesianStructureDefinition.pair_pi_compose [in interfaces.MonoidalCategory]
CartesianStructureDefinition.p1 [in interfaces.MonoidalCategory]
CartesianStructureDefinition.p1_pair [in interfaces.MonoidalCategory]
CartesianStructureDefinition.p2 [in interfaces.MonoidalCategory]
CartesianStructureDefinition.p2_pair [in interfaces.MonoidalCategory]
CartesianStructureDefinition.ter [in interfaces.MonoidalCategory]
CartesianStructureDefinition.ter_uni [in interfaces.MonoidalCategory]
CartesianStructureDefinition.unit [in interfaces.MonoidalCategory]
CategoryDefinition.compose [in interfaces.Category]
CategoryDefinition.compose_assoc [in interfaces.Category]
CategoryDefinition.compose_id_right [in interfaces.Category]
CategoryDefinition.compose_id_left [in interfaces.Category]
CategoryDefinition.id [in interfaces.Category]
CategoryDefinition.m [in interfaces.Category]
CategoryDefinition.t [in interfaces.Category]
CocartesianStructureDefinition.copair [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair_iota_compose [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair_i2 [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.copair_i1 [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.ini [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.ini_uni [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.i1 [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.i2 [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.omap [in interfaces.MonoidalCategory]
CocartesianStructureDefinition.unit [in interfaces.MonoidalCategory]
ConcreteCategoryDefinition.compose_mor [in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.id_mor [in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.Morphism [in interfaces.ConcreteCategory]
ConcreteCategoryDefinition.Structure [in interfaces.ConcreteCategory]
CoproductsDefinition.coprod [in interfaces.Limits]
CoproductsDefinition.cotuple [in interfaces.Limits]
CoproductsDefinition.cotuple_iota [in interfaces.Limits]
CoproductsDefinition.iota [in interfaces.Limits]
CoproductsDefinition.iota_cotuple [in interfaces.Limits]
E
Enriched.compose_mor_r [in interfaces.ConcreteCategory]Enriched.compose_mor_l [in interfaces.ConcreteCategory]
Enriched.hom_structure [in interfaces.ConcreteCategory]
F
Faithful.faithful [in interfaces.Functor]Full.full [in interfaces.Functor]
FunctorDefinition.fmap [in interfaces.Functor]
FunctorDefinition.fmap_compose [in interfaces.Functor]
FunctorDefinition.fmap_id [in interfaces.Functor]
FunctorDefinition.omap [in interfaces.Functor]
FunctorMonoidal.omap_prod_nat [in interfaces.MonoidalCategory]
FunctorMonoidal.omap_prod [in interfaces.MonoidalCategory]
FunctorMonoidal.omap_unit [in interfaces.MonoidalCategory]
J
JoinMeetDense.join_meet_dense [in lattices.FCD]JoinMeetDense.meet_join_dense [in lattices.FCD]
L
LatticeCategory.compose_mor [in structures.Completion]LatticeCategory.id_mor [in structures.Completion]
LatticeCategory.Morphism [in structures.Completion]
LatticeCategory.mor_ref [in structures.Completion]
LatticeCompletionSpec.emb [in structures.Completion]
LatticeCompletionSpec.emb_mor [in structures.Completion]
LatticeCompletionSpec.ext [in structures.Completion]
LatticeCompletionSpec.ext_unique [in structures.Completion]
LatticeCompletionSpec.ext_ana [in structures.Completion]
LatticeCompletionSpec.ext_mor [in structures.Completion]
LatticeCompletionSpec.F [in structures.Completion]
Limits.lim [in interfaces.Limits]
Limits.lim_spec [in interfaces.Limits]
M
MonoidalClosureDefinition.curry [in interfaces.MonoidalCategory]MonoidalClosureDefinition.curry_natural_r [in interfaces.MonoidalCategory]
MonoidalClosureDefinition.curry_natural_l [in interfaces.MonoidalCategory]
MonoidalClosureDefinition.curry_uncurry [in interfaces.MonoidalCategory]
MonoidalClosureDefinition.uncurry [in interfaces.MonoidalCategory]
MonoidalClosureDefinition.uncurry_curry [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.assoc [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.assoc_coh [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.assoc_nat [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.lunit [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.lunit_nat [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.runit [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.runit_nat [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.unit [in interfaces.MonoidalCategory]
MonoidalStructureDefinition.unit_coh [in interfaces.MonoidalCategory]
N
N [in examples.CAL]P
PreservesProducts.fmap_pi [in interfaces.Limits]PreservesProducts.omap_prod [in interfaces.Limits]
ProductsDefinition.pi [in interfaces.Limits]
ProductsDefinition.pi_tuple [in interfaces.Limits]
ProductsDefinition.prod [in interfaces.Limits]
ProductsDefinition.tuple [in interfaces.Limits]
ProductsDefinition.tuple_pi [in interfaces.Limits]
S
SymmetricMonoidalStructureDefinition.runit_swap [in interfaces.MonoidalCategory]SymmetricMonoidalStructureDefinition.swap [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap_swap [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap_assoc [in interfaces.MonoidalCategory]
SymmetricMonoidalStructureDefinition.swap_nat [in interfaces.MonoidalCategory]
V
val [in examples.CAL]Projection Index
A
ar [in models.Signature]ar [in models.IntStrat]
B
bind [in structures.Monad]bind_inf [in structures.Monad]
bind_sup [in structures.Monad]
bind_bind [in structures.Monad]
bind_ret [in structures.Monad]
bw [in models.IntStrat]
bw_fw [in models.IntStrat]
C
CategoryTheory.bw [in interfaces.Category]CategoryTheory.bw_fw [in interfaces.Category]
CategoryTheory.fw [in interfaces.Category]
CategoryTheory.fw_bw [in interfaces.Category]
cdcat_cat [in structures.Category]
cdl_poset [in structures.Lattice]
CDL.mor [in lattices.FCD]
coh [in models.Coherence]
coh_symm [in models.Coherence]
coh_refl [in models.Coherence]
compose [in structures.Category]
compose_mor_l [in structures.Category]
compose_mor_r [in structures.Category]
compose_assoc [in structures.Category]
compose_id [in structures.Category]
ConcreteCategoryTheory.apply [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.carrier [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.morphism [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.structure [in interfaces.ConcreteCategory]
D
dc_po [in models.DCPO]determinism [in models.IntStrat]
directed [in models.DCPO]
Downset.closed [in lattices.Downset]
Downset.has [in lattices.Downset]
dsup [in models.DCPO]
dsup_is_sup [in models.DCPO]
E
eop [in models.Signature]esig_ar [in models.Signature]
F
FunctorCategory.comp [in interfaces.FunctorCategory]FunctorCategory.fapply [in interfaces.FunctorCategory]
FunctorCategory.fapply_compose [in interfaces.FunctorCategory]
FunctorCategory.fapply_id [in interfaces.FunctorCategory]
FunctorCategory.natural [in interfaces.FunctorCategory]
FunctorCategory.oapply [in interfaces.FunctorCategory]
fw [in models.IntStrat]
fw_bw [in models.IntStrat]
G
get [in models.IntStrat]get_eqv [in models.IntStrat]
get_set [in models.IntStrat]
H
has [in models.Coherence]has_coh [in models.Coherence]
I
id [in structures.Category]id_compose [in structures.Category]
inf_glb [in structures.Lattice]
inf_lb [in structures.Lattice]
Inf.mor [in lattices.Upset]
init_state_eqv [in models.IntStrat]
init_state [in models.IntStrat]
intm_lmor [in structures.Effects]
iso_bw [in models.IntStrat]
iso_fw [in models.IntStrat]
L
Lazy.mor [in lattices.AdjoinBot]Lazy.mor_sup [in lattices.AdjoinBot]
lcdlm_sup [in structures.Effects]
lcdlm_inf [in structures.Effects]
le [in models.DCPO]
le_po [in models.DCPO]
le_preo [in models.DCPO]
LimitsPreliminaries.edge [in interfaces.Limits]
LimitsPreliminaries.edge_mor [in interfaces.Limits]
LimitsPreliminaries.face [in interfaces.Limits]
LimitsPreliminaries.lim_uni [in interfaces.Limits]
LimitsPreliminaries.lim_mor [in interfaces.Limits]
LimitsPreliminaries.vertex [in interfaces.Limits]
LimitsPreliminaries.vertex_mor [in interfaces.Limits]
LinCCALBase.ci_next [in models.LinCCAL]
LinCCALBase.ci_safe [in models.LinCCAL]
LinCCALBase.ci_valid [in models.LinCCAL]
LinCCALBase.correct_next [in models.LinCCAL]
LinCCALBase.correct_safe [in models.LinCCAL]
LinCCALBase.correct_valid [in models.LinCCAL]
LinCCALBase.li_correct [in models.LinCCAL]
LinCCALBase.li_impl [in models.LinCCAL]
LinCCALBase.li_spec [in models.LinCCAL]
LinCCALBase.li_sig [in models.LinCCAL]
LinCCALBase.Spec.next [in models.LinCCAL]
LinCCALBase.st_base [in models.LinCCAL]
LinCCALBase.st_impl [in models.LinCCAL]
LinCCALBase.st_spec [in models.LinCCAL]
LinCCALBase.ts_res [in models.LinCCAL]
LinCCALBase.ts_prog [in models.LinCCAL]
LinCCALBase.ts_op [in models.LinCCAL]
linf [in structures.Lattice]
lsup [in structures.Lattice]
M
Monoids.carrier [in interfaces.FunctorCategory]Monoids.eta [in interfaces.FunctorCategory]
Monoids.map [in interfaces.FunctorCategory]
Monoids.map_mu [in interfaces.FunctorCategory]
Monoids.map_eta [in interfaces.FunctorCategory]
Monoids.mu [in interfaces.FunctorCategory]
Monoids.mu_mu [in interfaces.FunctorCategory]
Monoids.mu_eta_r [in interfaces.FunctorCategory]
Monoids.mu_eta_l [in interfaces.FunctorCategory]
mor_monotonic [in structures.Poset]
mtens [in structures.Category]
O
op [in models.Signature]op [in structures.Effects]
op [in models.IntStrat]
operand [in models.Signature]
operand [in models.IntStrat]
operator [in models.Signature]
operator [in models.IntStrat]
op_mor [in structures.Effects]
op_lm [in structures.Effects]
P
poset_carrier [in structures.Poset]R
ref [in structures.Poset]ref_po [in structures.Poset]
ref_preo [in structures.Poset]
ret [in structures.Monad]
retraction [in models.IntStrat]
ret_bind [in structures.Monad]
S
sc_dsup_sup [in models.DCPO]set [in models.IntStrat]
set_eqv [in models.IntStrat]
set_set [in models.IntStrat]
set_get [in models.IntStrat]
SigBase.ar [in models.EffectSignatures]
SigBase.op [in models.EffectSignatures]
SigBase.operand [in models.EffectSignatures]
SigBase.operator [in models.EffectSignatures]
SigBase.prod_op [in models.EffectSignatures]
SigComp.Comp.ar_next [in models.EffectSignatures]
SigComp.Comp.ar_first [in models.EffectSignatures]
SigComp.Comp.op_next [in models.EffectSignatures]
SigComp.Comp.op_first [in models.EffectSignatures]
state [in models.IntStrat]
state_eqv [in models.IntStrat]
sup_inf [in structures.Lattice]
sup_lub [in structures.Lattice]
sup_ub [in structures.Lattice]
sup_lub [in models.DCPO]
sup_ub [in models.DCPO]
Sup.mor [in lattices.Downset]
T
tens [in structures.Category]token [in models.Coherence]
Inductive Index
B
bq_sig [in examples.CAL]C
ccpos [in models.IntStrat]CDL.Morphism [in lattices.FCD]
cepos [in models.IntStrat]
comp_has [in models.IntStrat]
cpos [in models.IntStrat]
csprod_coh [in models.Coherence]
cssum_coh [in models.Coherence]
D
dag_comult_lmaps [in models.Coherence]dag_counit_lmaps [in models.Coherence]
dag_lmaps [in models.Coherence]
Directed [in models.DCPO]
D2.m_def [in interfaces.Limits]
E
Ebq [in models.Signature]emor_rc_has [in models.IntStrat]
emor_has [in models.IntStrat]
empty_sig [in structures.Effects]
epos [in models.IntStrat]
Erb [in models.Signature]
esepos [in models.IntStrat]
esipos [in models.IntStrat]
esum [in structures.Effects]
F
fccpos [in models.IntStrat]fcomp_has [in models.IntStrat]
fcpos [in models.IntStrat]
fcrspos [in models.IntStrat]
I
im [in models.DCPO]Inf.Morphism [in lattices.Upset]
ISpec.play [in models.IntSpec]
ISpec.pref [in models.IntSpec]
L
Lazy.Morphism [in lattices.AdjoinBot]Lazy.NSupMorphism [in lattices.AdjoinBot]
LBot.opt [in lattices.AdjoinBot]
lcjepos [in models.IntStrat]
lcjipos [in models.IntStrat]
lcpepos [in models.IntStrat]
lcpipos [in models.IntStrat]
lens_has [in models.IntStrat]
LinCCALBase.comp_state_def [in models.LinCCAL]
LinCCALBase.comp_threadstate [in models.LinCCAL]
LinCCALBase.comp_phase [in models.LinCCAL]
LinCCALBase.estep [in models.LinCCAL]
LinCCALBase.id_state [in models.LinCCAL]
LinCCALBase.id_linstate [in models.LinCCAL]
LinCCALBase.lstep [in models.LinCCAL]
LinCCALBase.run_check_r [in models.LinCCAL]
LinCCALBase.run_check_l [in models.LinCCAL]
LinCCALBase.Spec.outcome [in models.LinCCAL]
LinCCALExample.Ecounter_op [in models.LinCCAL]
LinCCALExample.Elock_op [in models.LinCCAL]
LinCCALExample.Ereg_op [in models.LinCCAL]
LinCCALExample.fai_state [in models.LinCCAL]
LinCCALExample.fai_threadstate [in models.LinCCAL]
LinCCALTens.Tens.assoc_bw_state [in models.LinCCAL]
LinCCALTens.Tens.assoc_fw_state [in models.LinCCAL]
LinCCALTens.Tens.fmap_state [in models.LinCCAL]
LinCCALTens.Tens.fmap_threadstate [in models.LinCCAL]
LinCCALTens.Tens.iso_threadstate [in models.LinCCAL]
LinCCALTens.Tens.lunit_bw_state [in models.LinCCAL]
LinCCALTens.Tens.lunit_fw_state [in models.LinCCAL]
LinCCALTens.Tens.runit_bw_state [in models.LinCCAL]
LinCCALTens.Tens.runit_fw_state [in models.LinCCAL]
LinCCALTens.Tens.swap_state [in models.LinCCAL]
list_coh [in models.Coherence]
lneg_coh [in models.Coherence]
lneg_token [in models.Coherence]
lpos [in models.IntStrat]
lpos_eqv [in models.IntStrat]
M
move [in models.IntStrat]P
pcoh [in models.IntStrat]play [in models.IntStrat]
position [in models.IntStrat]
pref [in models.IntStrat]
R
rb_bq [in examples.CAL]rb_sig [in examples.CAL]
rcp [in models.IntStrat]
rcp_ref [in models.IntStrat]
rscpos [in models.IntStrat]
rsp [in models.IntStrat]
rspos [in models.IntStrat]
rsvpos [in models.IntStrat]
S
sccpos [in models.IntStrat]scipos [in models.IntStrat]
SigBase.eop [in models.EffectSignatures]
SigBase.sig_esig [in models.EffectSignatures]
SigBase.term [in models.EffectSignatures]
srunpos [in models.IntStrat]
state_sig [in examples.CAL]
Sup.Morphism [in lattices.Downset]
T
term [in models.Sets]testsig [in models.Sets]
tpos [in models.IntStrat]
trspos [in models.IntStrat]
tstrat_has [in models.IntStrat]
Two.m_def [in interfaces.Category]
V
VCOMP_NOT_ASSOC.foo_has [in models.IntStrat]Section Index
C
CDL.DEF [in lattices.FCD]COMPOSE [in models.IntStrat]
COMPOSE_FCOMP [in models.IntStrat]
COMPOSE_COMPOSE [in models.IntStrat]
COMPOSE_ID [in models.IntStrat]
D
Downset.DOWNSETS [in lattices.Downset]E
EMOR_RC [in models.IntStrat]EMOR_STRAT [in models.IntStrat]
ESTRAT_FCOMP [in models.IntStrat]
ESTRAT_COMPOSE [in models.IntStrat]
F
FCD.DEF [in lattices.FCD]FCOMP_RSQ [in models.IntStrat]
FCOMP_VCOMP [in models.IntStrat]
FCOMP_VID [in models.IntStrat]
FCOMP_RC [in models.IntStrat]
FCOMP_STRAT [in models.IntStrat]
FPAIR [in models.IntStrat]
I
ID_RSQ [in models.IntStrat]L
LatticeCompletionSpec.DEFS [in structures.Completion]Lazy.DEF [in lattices.AdjoinBot]
LBot.DEF [in lattices.AdjoinBot]
LENS_RC [in models.IntStrat]
LENS_STRAT_REF [in models.IntStrat]
LENS_STRAT [in models.IntStrat]
LinCCALBase.COMPOSE [in models.LinCCAL]
LinCCALTens.Tens.CORRECTNESS [in models.LinCCAL]
LinCCALTens.Tens.ISO_CORRECTNESS [in models.LinCCAL]
O
OPS [in structures.Lattice]P
PREDICATES [in structures.Lattice]PROPERTIES [in structures.Lattice]
R
RC [in models.IntStrat]RSQ [in models.IntStrat]
RSQ_COMP [in models.IntStrat]
RSVCOMP [in models.IntStrat]
S
SCOMP_COMPOSE [in models.IntStrat]SCOMP_ID [in models.IntStrat]
SRU_NATURAL [in models.IntStrat]
STRAT [in models.IntStrat]
STRAT.NEXT [in models.IntStrat]
T
TCONV [in models.IntStrat]TCONV_VCOMP [in models.IntStrat]
TENS_EMOR [in models.IntStrat]
TRSQ [in models.IntStrat]
TSTRAT [in models.IntStrat]
U
Upset.DEFS [in lattices.Upset]V
VCOMP [in models.IntStrat]VCOMP_VID [in models.IntStrat]
VID [in models.IntStrat]
Instance Index
B
bigop_eq [in models.IntSpec]C
CartesianStructureLimit.prod_c_lim [in interfaces.Limits]CDL.cmor_inf [in lattices.FCD]
CDL.cmor_sup [in lattices.FCD]
CDL.mor_ref [in lattices.FCD]
compose_deterministic [in models.IntStrat]
cSET.compose_mor [in interfaces.ConcreteCategory]
cSET.id_mor [in interfaces.ConcreteCategory]
D
DCPO.compose_mor [in models.DCPO]DCPO.id_mor [in models.DCPO]
Downset.ext_mor [in lattices.Downset]
F
fassoc_iso [in models.IntStrat]FCD.ext_mor [in lattices.FCD]
ffst_fdelta [in models.IntStrat]
flu_iso [in models.IntStrat]
fru_iso [in models.IntStrat]
fsnd_fdelta [in models.IntStrat]
fswap_iso [in models.IntStrat]
funext_rel [in models.IntStrat]
funext_subrel [in models.IntStrat]
I
im_directed [in models.DCPO]inf_eq [in models.IntStrat]
ISpec.apply_mor_params [in models.IntSpec]
ISpec.apply_mor [in models.IntSpec]
ISpec.bind_mor_params [in models.IntSpec]
ISpec.bind_mor [in models.IntSpec]
ISpec.papply_mor [in models.IntSpec]
ISpec.pbind_mor [in models.IntSpec]
ISpec.pref_antisym [in models.IntSpec]
ISpec.pref_preo [in models.IntSpec]
L
LatticeCompletionDefs.emb_params [in structures.Completion]LatticeCompletionDefs.emb_mor' [in structures.Completion]
LatticeCompletionDefs.ext_params [in structures.Completion]
LatticeCompletionDefs.map_params [in structures.Completion]
LatticeCompletionDefs.map_mor [in structures.Completion]
Lazy.cmor_inf [in lattices.AdjoinBot]
Lazy.cmor_sup [in lattices.AdjoinBot]
Lazy.mor_ref [in lattices.AdjoinBot]
LBot.emb_mor [in lattices.AdjoinBot]
LBot.ext_mor [in lattices.AdjoinBot]
lens_strat_eq [in models.IntStrat]
N
next_deterministic [in models.IntStrat]P
pcoh_sym [in models.IntStrat]pcoh_refl [in models.IntStrat]
Poset.compose_mor [in models.DCPO]
Poset.id_mor [in models.DCPO]
R
rcnext_params [in models.IntStrat]rcnext_ref [in models.IntStrat]
ref_po [in models.Coherence]
ref_preo [in models.Coherence]
rsp_params [in models.IntStrat]
rsp_ref [in models.IntStrat]
rsq_params [in models.IntStrat]
rsq_when_params [in models.IntStrat]
rsq_ref [in models.IntStrat]
rsq_when_ref [in models.IntStrat]
S
sassoc_iso [in models.IntStrat]scomp_strat_eq [in models.IntStrat]
scons_deterministic [in models.IntStrat]
sc_le [in models.DCPO]
SET [in structures.Category]
SET_prod [in structures.Category]
slens_eqv_equiv [in models.IntStrat]
slu_iso [in models.IntStrat]
sru_iso [in models.IntStrat]
stateful_play_mor [in examples.CAL]
sup_eq [in models.IntStrat]
U
Upset.ext_mor [in lattices.Upset]V
vcomp_has_ref [in models.IntStrat]Abbreviation Index
C
CartesianTheory.T [in interfaces.MonoidalCategory]compose [in models.IntStrat]
D
down [in lattices.Downset]downset [in lattices.Downset]
F
fcomp_st [in models.IntStrat]I
id [in models.IntStrat]ispec [in models.IntSpec]
L
lid [in models.IntStrat]LinCCALBase.spec [in models.LinCCAL]
LinCCALBase.Spec.lts [in models.LinCCAL]
LinCCALBase.star [in models.LinCCAL]
LinCCALBase.tid [in models.LinCCAL]
LinCCALBase.tmap [in models.LinCCAL]
M
MonoidalTheory.α [in interfaces.MonoidalCategory]MonoidalTheory.λ [in interfaces.MonoidalCategory]
MonoidalTheory.ρ [in interfaces.MonoidalCategory]
S
SymmetricMonoidalTheory.γ [in interfaces.MonoidalCategory]T
tstrat [in models.IntStrat]U
up [in lattices.Upset]upset [in lattices.Upset]
Definition Index
A
amap [in models.Signature]assert [in examples.CAL]
B
basis [in models.Signature]bcomp [in models.IntStrat]
bid [in models.IntStrat]
BifunctorTheory.fmap_iso [in interfaces.Functor]
BifunctorTheory.PF.fmap [in interfaces.Functor]
BifunctorTheory.PF.omap [in interfaces.Functor]
bij_lens [in models.IntStrat]
bot [in structures.Lattice]
bot [in models.Coherence]
bq_state [in examples.CAL]
C
CALspec [in examples.CAL]CALspec_mor [in examples.CAL]
CartesianStructureFromProducts.omap [in interfaces.Limits]
CartesianStructureFromProducts.pair [in interfaces.Limits]
CartesianStructureFromProducts.p1 [in interfaces.Limits]
CartesianStructureFromProducts.p2 [in interfaces.Limits]
CartesianStructureFromProducts.ter [in interfaces.Limits]
CartesianStructureFromProducts.unit [in interfaces.Limits]
CartesianStructureLimit.prod_c [in interfaces.Limits]
CartesianStructureLimit.prod_d [in interfaces.Limits]
CartesianStructureTheory.assoc [in interfaces.MonoidalCategory]
CartesianStructureTheory.fmap [in interfaces.MonoidalCategory]
CartesianStructureTheory.lunit [in interfaces.MonoidalCategory]
CartesianStructureTheory.runit [in interfaces.MonoidalCategory]
CartesianStructureTheory.swap [in interfaces.MonoidalCategory]
CategoryTheory.bw_iso [in interfaces.Category]
CategoryTheory.compose_iso [in interfaces.Category]
CategoryTheory.id_iso [in interfaces.Category]
cdlat_prod [in lattices.LatticeProduct]
CocartesianStructureTheory.assoc [in interfaces.MonoidalCategory]
CocartesianStructureTheory.fmap [in interfaces.MonoidalCategory]
CocartesianStructureTheory.lunit [in interfaces.MonoidalCategory]
CocartesianStructureTheory.runit [in interfaces.MonoidalCategory]
CocartesianStructureTheory.swap [in interfaces.MonoidalCategory]
combine_ans [in models.IntStrat]
compose_when [in models.IntStrat]
ConcreteCategoryTheory.compose [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.id [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.m [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.t [in interfaces.ConcreteCategory]
conv [in models.IntStrat]
copair [in models.Coherence]
cSET.Morphism [in interfaces.ConcreteCategory]
cSET.Structure [in interfaces.ConcreteCategory]
csi1 [in models.Coherence]
csi2 [in models.Coherence]
cspair [in models.Coherence]
csprod [in models.Coherence]
csp1 [in models.Coherence]
csp2 [in models.Coherence]
cssum [in models.Coherence]
cstens [in models.Coherence]
cstens_lmap [in models.Coherence]
csterm [in models.Coherence]
csunit [in models.Coherence]
D
dag [in models.Coherence]dag_ext [in models.Coherence]
dag_comult [in models.Coherence]
dag_counit [in models.Coherence]
dag_lmap [in models.Coherence]
DCPO.Morphism [in models.DCPO]
DCPO.Structure [in models.DCPO]
directed [in models.Coherence]
discard [in models.Coherence]
discrete [in models.Signature]
dmor [in models.Signature]
Downset.emb [in lattices.Downset]
Downset.ext [in lattices.Downset]
Downset.F [in lattices.Downset]
Downset.Fpos [in lattices.Downset]
D2.compose [in interfaces.Limits]
D2.id [in interfaces.Limits]
D2.m [in interfaces.Limits]
D2.t [in interfaces.Limits]
E
ecomp [in models.IntStrat]eid [in models.IntStrat]
emor [in models.IntStrat]
emor_rc [in models.IntStrat]
emor_strat [in models.IntStrat]
emor_when [in models.IntStrat]
Empty_sig [in models.IntStrat]
encap [in models.IntStrat]
EndofunctorComposition.Tens.assoc [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.lunit [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.runit [in interfaces.FunctorCategory]
EndofunctorComposition.Tens.unit [in interfaces.FunctorCategory]
esig [in structures.Effects]
esig_sig [in models.Signature]
ex1 [in models.Signature]
ex2 [in models.Signature]
F
fassoc [in models.IntStrat]fassocr [in models.IntStrat]
FCD.emb [in lattices.FCD]
FCD.ext [in lattices.FCD]
FCD.F [in lattices.FCD]
fcomp [in models.IntStrat]
fcomp_rc [in models.IntStrat]
fcomp_rc_has [in models.IntStrat]
fcomp_when [in models.IntStrat]
fcomp_emor [in models.IntStrat]
fdrop [in models.IntStrat]
fdup [in models.IntStrat]
ffst [in models.IntStrat]
finf [in structures.Lattice]
flu [in models.IntStrat]
flur [in models.IntStrat]
fpair [in models.IntStrat]
free_m [in models.Sets]
free_f [in models.Sets]
fru [in models.IntStrat]
frur [in models.IntStrat]
fsnd [in models.IntStrat]
fsup [in structures.Lattice]
fswap [in models.IntStrat]
FunctorCategory.compose [in interfaces.FunctorCategory]
FunctorCategory.id [in interfaces.FunctorCategory]
FunctorCategory.m [in interfaces.FunctorCategory]
FunctorCategory.t [in interfaces.FunctorCategory]
FunctorComposition.fmap [in interfaces.FunctorCategory]
FunctorComposition.omap [in interfaces.FunctorCategory]
FunctorTheory.fmap_iso [in interfaces.Functor]
G
glob [in models.IntStrat]H
hmap [in models.Signature]I
id_cpos_r [in models.IntStrat]id_idpos_r [in models.IntStrat]
id_pos_r [in models.IntStrat]
id_cpos_l [in models.IntStrat]
id_idpos_l [in models.IntStrat]
id_pos_l [in models.IntStrat]
imap [in models.Coherence]
input [in models.Coherence]
inv [in models.IntStrat]
ISpec.apply [in models.IntSpec]
ISpec.bind [in models.IntSpec]
ISpec.compose [in models.IntSpec]
ISpec.int [in models.IntSpec]
ISpec.papply [in models.IntSpec]
ISpec.pbind [in models.IntSpec]
ISpec.play_poset [in models.IntSpec]
ISpec.ret [in models.IntSpec]
ISpec.subst [in models.IntSpec]
ISpec.t [in models.IntSpec]
J
join [in structures.Lattice]L
LatticeCompletionDefs.map [in structures.Completion]layer [in examples.CAL]
LBot.emb [in lattices.AdjoinBot]
LBot.ext [in lattices.AdjoinBot]
LBot.F [in lattices.AdjoinBot]
LBot.Fposet [in lattices.AdjoinBot]
LBot.inf_sup_of [in lattices.AdjoinBot]
LBot.inf_of [in lattices.AdjoinBot]
LBot.is [in lattices.AdjoinBot]
LBot.proj [in lattices.AdjoinBot]
LBot.sup_inf_of [in lattices.AdjoinBot]
LBot.sup_of [in lattices.AdjoinBot]
lcj [in models.IntStrat]
lcj_when [in models.IntStrat]
lcj_has [in models.IntStrat]
lcomp [in models.IntStrat]
lconv [in models.IntStrat]
lcp [in models.IntStrat]
lcp_when [in models.IntStrat]
lcp_has [in models.IntStrat]
ldrop [in models.IntStrat]
lens_strat [in models.IntStrat]
lens_strat_when [in models.IntStrat]
lim [in models.Coherence]
LinCCALBase.cal [in models.LinCCAL]
LinCCALBase.compose [in models.LinCCAL]
LinCCALBase.comp_state [in models.LinCCAL]
LinCCALBase.comp_tmap [in models.LinCCAL]
LinCCALBase.id [in models.LinCCAL]
LinCCALBase.m [in models.LinCCAL]
LinCCALBase.pending_program [in models.LinCCAL]
LinCCALBase.reachable [in models.LinCCAL]
LinCCALBase.specified [in models.LinCCAL]
LinCCALBase.Spec.gen [in models.LinCCAL]
LinCCALBase.Spec.tens [in models.LinCCAL]
LinCCALBase.Spec.tens_lts [in models.LinCCAL]
LinCCALBase.t [in models.LinCCAL]
LinCCALBase.threadstate_valid [in models.LinCCAL]
LinCCALExample.Ecounter [in models.LinCCAL]
LinCCALExample.Elock [in models.LinCCAL]
LinCCALExample.Ereg [in models.LinCCAL]
LinCCALExample.Ereg_ar [in models.LinCCAL]
LinCCALExample.fai_impl [in models.LinCCAL]
LinCCALExample.Lcounter [in models.LinCCAL]
LinCCALExample.Llock [in models.LinCCAL]
LinCCALExample.Lreg [in models.LinCCAL]
LinCCALExample.Mcounter [in models.LinCCAL]
LinCCALExample.Σcounter [in models.LinCCAL]
LinCCALExample.Σlock [in models.LinCCAL]
LinCCALExample.Σreg [in models.LinCCAL]
LinCCALTens.Tens.assoc [in models.LinCCAL]
LinCCALTens.Tens.fmap [in models.LinCCAL]
LinCCALTens.Tens.fmap_tmap [in models.LinCCAL]
LinCCALTens.Tens.iso_tmap [in models.LinCCAL]
LinCCALTens.Tens.lunit [in models.LinCCAL]
LinCCALTens.Tens.omap [in models.LinCCAL]
LinCCALTens.Tens.runit [in models.LinCCAL]
LinCCALTens.Tens.swap [in models.LinCCAL]
LinCCALTens.Tens.unit [in models.LinCCAL]
lmap [in models.Coherence]
lmap_flip [in models.Coherence]
lmap_apply [in models.Coherence]
lmap_compose [in models.Coherence]
lmap_id [in models.Coherence]
lneg [in models.Coherence]
lsq [in models.IntStrat]
L_rb [in examples.CAL]
L_bq [in examples.CAL]
M
meet [in structures.Lattice]Monoids.compose [in interfaces.FunctorCategory]
Monoids.id [in interfaces.FunctorCategory]
Monoids.m [in interfaces.FunctorCategory]
Monoids.t [in interfaces.FunctorCategory]
M_bq [in examples.CAL]
N
next [in models.IntStrat]O
oext [in models.Coherence]omap [in models.Coherence]
One.compose [in interfaces.Category]
One.id [in interfaces.Category]
One.m [in interfaces.Category]
One.t [in interfaces.Category]
OppositeCategory.compose [in interfaces.Category]
OppositeCategory.id [in interfaces.Category]
OppositeCategory.m [in interfaces.Category]
OppositeCategory.t [in interfaces.Category]
oret [in models.Coherence]
output [in models.Coherence]
P
passoc [in models.IntStrat]play_poset [in models.IntStrat]
plu [in models.IntStrat]
poset_prod [in lattices.LatticeProduct]
Poset.Morphism [in models.DCPO]
Poset.Structure [in models.DCPO]
prod_lens [in models.IntStrat]
prod_bij [in models.IntStrat]
Prod.compose [in interfaces.Category]
Prod.id [in interfaces.Category]
Prod.m [in interfaces.Category]
Prod.t [in interfaces.Category]
pru [in models.IntStrat]
pswap [in models.IntStrat]
R
rb_state [in examples.CAL]rcnext [in models.IntStrat]
rcp_poset [in models.IntStrat]
ref [in models.Coherence]
RegBase.compose [in models.EffectSignatures]
RegBase.id [in models.EffectSignatures]
RegBase.m [in models.EffectSignatures]
RegBase.t [in models.EffectSignatures]
RegBase.transform [in models.EffectSignatures]
RegPlus.Plus.copair [in models.EffectSignatures]
RegPlus.Plus.ini [in models.EffectSignatures]
RegPlus.Plus.i1 [in models.EffectSignatures]
RegPlus.Plus.i2 [in models.EffectSignatures]
RegPlus.Plus.omap [in models.EffectSignatures]
RegPlus.Plus.unit [in models.EffectSignatures]
rsq [in models.IntStrat]
rsq_when [in models.IntStrat]
S
sassoc [in models.IntStrat]sassocr [in models.IntStrat]
scomp [in models.IntStrat]
scomp_conv [in models.IntStrat]
scomp_strat [in models.IntStrat]
scons [in models.IntStrat]
seq [in models.Coherence]
seq_lmap [in models.Coherence]
SetBase.compose [in models.Sets]
SetBase.id [in models.Sets]
SetBase.m [in models.Sets]
SetBase.t [in models.Sets]
SetMonoidalStructures.Exp.curry [in models.Sets]
SetMonoidalStructures.Exp.fmap [in models.Sets]
SetMonoidalStructures.Exp.omap [in models.Sets]
SetMonoidalStructures.Exp.uncurry [in models.Sets]
SetMonoidalStructures.Prod.omap [in models.Sets]
SetMonoidalStructures.Prod.pair [in models.Sets]
SetMonoidalStructures.Prod.p1 [in models.Sets]
SetMonoidalStructures.Prod.p2 [in models.Sets]
SetMonoidalStructures.Prod.ter [in models.Sets]
SetMonoidalStructures.Prod.unit [in models.Sets]
SET.compose [in interfaces.Category]
SET.id [in interfaces.Category]
SET.m [in interfaces.Category]
SET.t [in interfaces.Category]
SigBase.amap [in models.EffectSignatures]
SigBase.compose [in models.EffectSignatures]
SigBase.coprod [in models.EffectSignatures]
SigBase.cotuple [in models.EffectSignatures]
SigBase.ear [in models.EffectSignatures]
SigBase.esig [in models.EffectSignatures]
SigBase.esig_sig [in models.EffectSignatures]
SigBase.hmap [in models.EffectSignatures]
SigBase.id [in models.EffectSignatures]
SigBase.iota [in models.EffectSignatures]
SigBase.m [in models.EffectSignatures]
SigBase.pi [in models.EffectSignatures]
SigBase.prod [in models.EffectSignatures]
SigBase.subst [in models.EffectSignatures]
SigBase.t [in models.EffectSignatures]
SigBase.tmap [in models.EffectSignatures]
SigBase.tmul [in models.EffectSignatures]
SigBase.transform [in models.EffectSignatures]
SigBase.tuple [in models.EffectSignatures]
sigcomp [in models.Signature]
SigComp.Comp.assoc [in models.EffectSignatures]
SigComp.Comp.fmap [in models.EffectSignatures]
SigComp.Comp.lunit [in models.EffectSignatures]
SigComp.Comp.omap [in models.EffectSignatures]
SigComp.Comp.runit [in models.EffectSignatures]
SigComp.Comp.unit [in models.EffectSignatures]
SigEnd.fmap [in models.EffectSignatures]
SigEnd.omap [in models.EffectSignatures]
sighom [in models.Signature]
sigi [in models.Signature]
sigid [in models.Signature]
siginl [in models.Signature]
siginr [in models.Signature]
SigMnd.fmap [in models.EffectSignatures]
SigMnd.omap [in models.EffectSignatures]
sigo [in models.Signature]
SigPlus.Plus.copair [in models.EffectSignatures]
SigPlus.Plus.ini [in models.EffectSignatures]
SigPlus.Plus.i1 [in models.EffectSignatures]
SigPlus.Plus.i2 [in models.EffectSignatures]
SigPlus.Plus.omap [in models.EffectSignatures]
SigPlus.Plus.unit [in models.EffectSignatures]
SigReg.fmap [in models.EffectSignatures]
SigReg.omap [in models.EffectSignatures]
sigsum [in models.Signature]
sigtens [in models.Signature]
SigTens.Tens.assoc [in models.EffectSignatures]
SigTens.Tens.fmap [in models.EffectSignatures]
SigTens.Tens.lunit [in models.EffectSignatures]
SigTens.Tens.omap [in models.EffectSignatures]
SigTens.Tens.runit [in models.EffectSignatures]
SigTens.Tens.swap [in models.EffectSignatures]
SigTens.Tens.unit [in models.EffectSignatures]
sigtup [in models.Signature]
slice [in examples.CAL]
slift [in examples.CAL]
slu [in models.IntStrat]
slur [in models.IntStrat]
srel_pull [in examples.CAL]
srel_push [in examples.CAL]
sru [in models.IntStrat]
srun [in examples.CAL]
srur [in models.IntStrat]
stateful_play [in examples.CAL]
strat [in models.IntStrat]
subst [in models.Sets]
SymmetricMonoidalStructureTheory.swap_iso [in interfaces.MonoidalCategory]
T
tassoc [in models.IntStrat]tassocr [in models.IntStrat]
tconv [in models.IntStrat]
tconv_has [in models.IntStrat]
tens [in models.IntStrat]
tens_emor [in models.IntStrat]
test [in models.Sets]
tlu [in models.IntStrat]
tlur [in models.IntStrat]
tmap [in models.Sets]
top [in structures.Lattice]
tru [in models.IntStrat]
trur [in models.IntStrat]
tstrat_when [in models.IntStrat]
tswap [in models.IntStrat]
Two.compose [in interfaces.Category]
Two.id [in interfaces.Category]
Two.m [in interfaces.Category]
Two.t [in interfaces.Category]
U
Unnamed_thm [in examples.CAL]update [in examples.CAL]
Upset.emb [in lattices.Upset]
Upset.ext [in lattices.Upset]
Upset.F [in lattices.Upset]
Upset.opp_cdlat [in lattices.Upset]
Upset.opp_poset [in lattices.Upset]
V
vcomp [in models.IntStrat]VCOMP_NOT_ASSOC.S [in models.IntStrat]
VCOMP_NOT_ASSOC.foo [in models.IntStrat]
VCOMP_NOT_ASSOC.R [in models.IntStrat]
VCOMP_NOT_ASSOC.toprc_has [in models.IntStrat]
VCOMP_NOT_ASSOC.twoq [in models.IntStrat]
VCOMP_NOT_ASSOC.twoa [in models.IntStrat]
VCOMP_NOT_ASSOC.one [in models.IntStrat]
vcomp_at [in models.IntStrat]
vcomp_at_has [in models.IntStrat]
vcomp_has [in models.IntStrat]
vid [in models.IntStrat]
vid_has [in models.IntStrat]
Z
Zero.compose [in interfaces.Category]Zero.id [in interfaces.Category]
Zero.m [in interfaces.Category]
Zero.t [in interfaces.Category]
Record Index
A
application [in models.Signature]application [in models.IntStrat]
B
bijection [in models.IntStrat]C
Category [in structures.Category]CategoryTheory.iso [in interfaces.Category]
CDCat [in structures.Category]
cdlattice [in structures.Lattice]
CDL.Morphism [in lattices.FCD]
CDMonad [in structures.Monad]
clique [in models.Coherence]
ConcreteCategoryTheory.structured_map [in interfaces.ConcreteCategory]
ConcreteCategoryTheory.structured_set [in interfaces.ConcreteCategory]
D
Deterministic [in models.IntStrat]Directed [in models.DCPO]
DirectedComplete [in models.DCPO]
Downset.downset [in lattices.Downset]
E
esig [in models.IntStrat]esig_op [in models.Signature]
F
FunctorCategory.functor [in interfaces.FunctorCategory]FunctorCategory.nt [in interfaces.FunctorCategory]
I
Inf.Morphism [in lattices.Upset]interp [in structures.Effects]
InterpMorphism [in structures.Effects]
Isomorphism [in models.IntStrat]
IsSup [in models.DCPO]
L
LazyMorphism [in structures.Effects]Lazy.Morphism [in lattices.AdjoinBot]
Lazy.NSupMorphism [in lattices.AdjoinBot]
lens [in models.IntStrat]
lens_eqv [in models.IntStrat]
LimitsPreliminaries.cone [in interfaces.Limits]
LimitsPreliminaries.cone_mor [in interfaces.Limits]
LimitsPreliminaries.Limit [in interfaces.Limits]
LinCCALBase.correct [in models.LinCCAL]
LinCCALBase.correctness_invariant [in models.LinCCAL]
LinCCALBase.layer_implementation [in models.LinCCAL]
LinCCALBase.layer_interface [in models.LinCCAL]
LinCCALBase.Spec.t [in models.LinCCAL]
LinCCALBase.state [in models.LinCCAL]
LinCCALBase.threadstate [in models.LinCCAL]
M
Monoids.mh [in interfaces.FunctorCategory]Monoids.mon [in interfaces.FunctorCategory]
P
PartialOrder [in models.DCPO]poset [in structures.Poset]
PosetMorphism [in structures.Poset]
R
Retraction [in models.IntStrat]S
ScottContinuous [in models.DCPO]sig [in models.Signature]
SigBase.application [in models.EffectSignatures]
SigBase.ops [in models.EffectSignatures]
SigBase.sig [in models.EffectSignatures]
SigComp.Comp.ar [in models.EffectSignatures]
SigComp.Comp.op [in models.EffectSignatures]
SMCat [in structures.Category]
space [in models.Coherence]
Sup.Morphism [in lattices.Downset]
| 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 | (2070 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 | (106 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 | (149 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 | (26 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 | (595 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 | (266 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 | (96 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 | (144 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 | (96 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 | (48 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 | (69 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 | (20 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 | (399 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 | (56 entries) |
This page has been generated by coqdoc