Free Choice atoms — typed substrate for FC scenarios #
Three typed propositional atoms shared across free-choice studies. Replaces
ad-hoc string atoms ("coffee", "tea", etc.) in scenario constructions
where a typo silently compiles to false under the
match p with | "coffee" => ... | _ => false fallthrough pattern endemic
to BSML- and Hamblin-style models.
a and b cover the disjuncts of binary FC inferences (α ∨ β, ◇(α ∨ β),
◇α ∨ ◇β). c is reserved for embedded scenarios involving a third
proposition (e.g. (◇(α ∨ β) ∨ ◇c) ∧ ¬◇c in Aloni 2022 §7 (55)).
This is substrate-level typing — Studies files instantiate BSMLModel's
String-keyed val field by pattern-matching on the canonical names
("a", "b", "c") and routing through these atoms via per-world holds
helpers. Eliminating the String layer entirely (i.e., making
BSMLModel.val : FCAtom → α → Bool) would require parameterizing
BSMLFormula and BSMLModel over the atom type — a substrate-wide
refactor deferred to a separate effort.
Equations
- Phenomena.FreeChoice.instDecidableEqFCAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Phenomena.FreeChoice.instReprFCAtom = { reprPrec := Phenomena.FreeChoice.instReprFCAtom.repr }
Equations
- One or more equations did not get rendered due to their size.
Canonical String name of an atom. Used at BSMLModel.val boundaries
where the substrate's val : String → α → Bool field forces String.