Elliott & Sudo (2025): Free Choice with Anaphora

[ES25a]

Bilateral Update Semantics (BUS) applied to bathroom disjunctions.

The puzzle

Bathroom disjunction: "Either there's no bathroom or it's in a funny place."

From this, we infer:

1. It's possible there's no bathroom
2. It's possible there's a bathroom AND it's in a funny place

The pronoun "it" in the second disjunct is bound by the existential in the negated first disjunct. This cross-disjunct anaphora is puzzling because:

• Standard FC: ◇(φ ∨ ψ) → ◇φ ∧ ◇ψ (no anaphoric connection)
• With anaphora: ◇(¬∃xφ ∨ ψ(x)) → ◇¬∃xφ ∧ ◇(∃x(φ ∧ ψ(x)))

Solution

BUS + Modal Disjunction:

1. Disjunction semantics: φ ∨ ψ entails ◇φ ∧ ◇ψ
2. Negation swaps positive/negative: ¬∃xφ positive = ∃xφ negative
3. Cross-disjunct binding: x introduced in ¬∃xφ is visible to ψ(x)

Key results

• Modified FC: ◇(φ ∨ ψ) ⊨ ◇φ ∧ ◇(¬φ ∧ ψ) (the paper's (95))
• FC with anaphora: bathroom inference pattern
• Dual prohibition: ¬◇φ ∧ ¬◇ψ ⊨ ¬(φ ∨ ψ) (preserved)

The paper's disjPos1/disjPos2 (eq. 92) recover the standard positive update as their union (disjStd_positive_eq, eq. 92c) and simplify for the bathroom case (eqs. 93–94):

• disjPos1 ⊆ s[∃ₓB(x)]⁻ (eq. 93)
• disjPos2 ⊆ s[∃ₓB(x)]⁺[F(x)]⁺ (eq. 94)

Under these simplification conditions, the general FC preconditions (both disjPos nonempty, eq. 96) yield the bathroom inference.

Bilateral Update Semantics

BUS ([Ell23], [ES25a]): dynamic semantics with two update dimensions (positive, negative) that validates DNE and handles cross-disjunct anaphora. A BUSDen is a BilateralDen at register-form variables; the operations here add presupposition (hasGap, defined), entailment (strawsonEntails, strongEntails), and epistemic modality (diamond, box, the paper's (73)/(77)).

@[reducible, inline]

abbrev ElliottSudo2025.BUSDen (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

BUS denotation: a bilateral denotation over register-keyed possibilities.

Equations

• ElliottSudo2025.BUSDen W E = DynamicSemantics.BilateralDen W ℕ E

def ElliottSudo2025.BUSDen.hasGap {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Prop

Truth-value gap: presupposition failure.

Equations

• φ.hasGap s = (φ.positive s ∪ φ.negative s ⊂ s)

def ElliottSudo2025.BUSDen.defined {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Prop

Sentence is defined (no presupposition failure).

Equations

• φ.defined s = (φ.positive s ∪ φ.negative s = s)

def ElliottSudo2025.BUSDen.skConj {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Strong Kleene conjunction.

Equations

• φ.skConj ψ = φ ⊙ ψ

def ElliottSudo2025.BUSDen.pConj {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Presupposition-preserving conjunction.

Equations

• One or more equations did not get rendered due to their size.

def ElliottSudo2025.BUSDen.strawsonEntails {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : Prop

Strawson entailment: φ entails ψ when φ is defined and true.

Equations

• φ.strawsonEntails ψ = ∀ (s : Set (DynamicSemantics.Possibility W ℕ (Part E))), φ.defined s → (φ.positive s).Nonempty → φ.positive s ⊆ ψ.positive (φ.positive s)

def ElliottSudo2025.BUSDen.strongEntails {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : Prop

Strong entailment: φ entails ψ with no presupposition failure.

Equations

• φ.strongEntails ψ = ∀ (s : Set (DynamicSemantics.Possibility W ℕ (Part E))), (φ.positive s).Nonempty → ψ.defined (φ.positive s) ∧ φ.positive s ⊆ ψ.positive (φ.positive s)

theorem ElliottSudo2025.BUSDen.neg_positive_eq_negative {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ : BUSDen W E) : (~φ).positive s = φ.negative s

theorem ElliottSudo2025.BUSDen.neg_negative_eq_positive {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ : BUSDen W E) : (~φ).negative s = φ.positive s

theorem ElliottSudo2025.BUSDen.disj_negative {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ ψ : BUSDen W E) : (φ ⊕ ψ).negative s = ψ.negative (φ.negative s)

def ElliottSudo2025.BUSDen.diamond {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : BUSDen W E

Epistemic possibility ([ES25a], (73)): the positive update returns s when the prejacent's positive update is consistent; the negative update returns s when the denial is already implicit in s, modulo introduced anaphoric information — state-level subsistence.

Equations

• One or more equations did not get rendered due to their size.

def ElliottSudo2025.BUSDen.box {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : BUSDen W E

Epistemic necessity ([ES25a], (77)): the dual, □φ = ¬◇¬φ.

Equations

• □ᵇφ = ~◇ᵇ~φ

def ElliottSudo2025.BUSDen.«term◇ᵇ_» : Lean.ParserDescr

Epistemic possibility ([ES25a], (73)): the positive update returns s when the prejacent's positive update is consistent; the negative update returns s when the denial is already implicit in s, modulo introduced anaphoric information — state-level subsistence.

Equations

• One or more equations did not get rendered due to their size.

def ElliottSudo2025.BUSDen.«term□ᵇ_» : Lean.ParserDescr

Epistemic necessity ([ES25a], (77)): the dual, □φ = ¬◇¬φ.

Equations

• One or more equations did not get rendered due to their size.

theorem ElliottSudo2025.BUSDen.diamond_positive_eq {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : (◇ᵇφ).positive s = if (φ.positive s).Nonempty then s else ∅

The diamond's positive update as a conditional: s if the prejacent is possible, absurd otherwise.

theorem ElliottSudo2025.BUSDen.diamond_negative_eq {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : (◇ᵇφ).negative s = if lowerClosure s ≤ lowerClosure (φ.negative s) then s else ∅

The diamond's negative update as a conditional.

theorem ElliottSudo2025.BUSDen.diamond_positive_isTest {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : DynamicSemantics.CCP.IsTest (◇ᵇφ).positive

Diamond positive is a test (returns s or ∅).

theorem ElliottSudo2025.BUSDen.diamond_negative_isTest {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : DynamicSemantics.CCP.IsTest (◇ᵇφ).negative

Diamond negative is a test (returns s or ∅).

theorem ElliottSudo2025.BUSDen.diamond_positive_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : DynamicSemantics.CCP.IsEliminative (◇ᵇφ).positive

Diamond positive is eliminative (from IsTest).

theorem ElliottSudo2025.BUSDen.diamond_positive_subset {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : (◇ᵇφ).positive s ⊆ s

Diamond positive subset (convenience form).

theorem ElliottSudo2025.BUSDen.diamond_negative_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : DynamicSemantics.CCP.IsEliminative (◇ᵇφ).negative

Diamond negative is eliminative (from IsTest).

theorem ElliottSudo2025.BUSDen.diamond_negative_subset {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : (◇ᵇφ).negative s ⊆ s

Diamond negative subset (convenience form).

theorem ElliottSudo2025.BUSDen.box_positive_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : DynamicSemantics.CCP.IsEliminative (□ᵇφ).positive

Box positive is eliminative (□φ = ¬◇¬φ, so positive = diamond negative of ¬φ).

theorem ElliottSudo2025.BUSDen.box_negative_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : DynamicSemantics.CCP.IsEliminative (□ᵇφ).negative

Box negative is eliminative.

Modality concepts

def ElliottSudo2025.possible {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Prop

Possibility: state s makes ◇φ true iff s[φ]⁺ is consistent.

Equations

• ElliottSudo2025.possible φ s = (φ.positive s).Nonempty

def ElliottSudo2025.necessary {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Prop

Necessity: state s makes □φ true iff s subsists in s[φ]⁺.

Equations

• ElliottSudo2025.necessary φ s = (lowerClosure s ≤ lowerClosure (φ.positive s))

def ElliottSudo2025.impossible {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Prop

Impossibility: ¬◇φ iff s[φ]⁺ is empty.

Equations

• ElliottSudo2025.impossible φ s = ¬(φ.positive s).Nonempty

theorem ElliottSudo2025.impossible_iff_empty {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ : BUSDen W E) : impossible φ s ↔ φ.positive s = ∅

Modal disjunction (anaphora-sensitive)

def ElliottSudo2025.disjStd {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Standard disjunction: the basic bilateral disjunction without FC preconditions.

Equations

• ElliottSudo2025.disjStd φ ψ = φ ⊕ ψ

def ElliottSudo2025.disjPos1 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Set (DynamicSemantics.Possibility W ℕ (Part E))

The part of the standard disjunction positive update that the first disjunct is responsible for: the (1,*) row of the Strong Kleene truth table.

s[φ ∨ ψ]₁⁺ = s[φ]⁺[ψ]⁺ ∪ s[φ]⁺[ψ]⁻ ∪ s[φ]⁺[ψ]?

Every possibility in s[φ]⁺ is verified by φ, and then classified by ψ into one of three truth values. (eq. 92a)

Equations

• ElliottSudo2025.disjPos1 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.negative (φ.positive s) ∪ DynamicSemantics.BilateralDen.unknownUpdate ψ (φ.positive s)

def ElliottSudo2025.disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : Set (DynamicSemantics.Possibility W ℕ (Part E))

The part of the standard disjunction positive update that the second disjunct is responsible for: the (*,1) column of the Strong Kleene truth table.

s[φ ∨ ψ]₂⁺ = s[φ]⁺[ψ]⁺ ∪ s[φ]⁻[ψ]⁺ ∪ s[φ]?[ψ]⁺

The key term for cross-disjunct anaphora is s[φ]⁻[ψ]⁺: when φ = ¬∃x.P(x), s[φ]⁻ = s[∃x.P(x)]⁺ by DNE, introducing the discourse referent for binding across disjuncts. (eq. 92b)

Equations

• ElliottSudo2025.disjPos2 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.positive (φ.negative s) ∪ ψ.positive (DynamicSemantics.BilateralDen.unknownUpdate φ s)

theorem ElliottSudo2025.disjStd_positive_eq {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : (disjStd φ ψ).positive s = disjPos1 φ ψ s ∪ disjPos2 φ ψ s

(92c): the standard positive update is the union of the parts the two disjuncts are responsible for.

def ElliottSudo2025.disjModal {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Modal Disjunction (anaphora-sensitive version, eq. 96): semantic disjunction that validates FC with anaphora, adding the precondition that each disjunct contribute at least some possibilities. This semantically derives FC without pragmatic reasoning.

Equations

• One or more equations did not get rendered due to their size.

def ElliottSudo2025.«term_∨ᶠᶜ_» : Lean.TrailingParserDescr

Modal Disjunction (anaphora-sensitive version, eq. 96): semantic disjunction that validates FC with anaphora, adding the precondition that each disjunct contribute at least some possibilities. This semantically derives FC without pragmatic reasoning.

Equations

• ElliottSudo2025.«term_∨ᶠᶜ_» = Lean.ParserDescr.trailingNode `ElliottSudo2025.«term_∨ᶠᶜ_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ᶠᶜ ") (Lean.ParserDescr.cat `term 0))

theorem ElliottSudo2025.neg_subset_disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) : ψ.positive (φ.negative s) ⊆ disjPos2 φ ψ s

ψ.positive (φ.negative s) ⊆ disjPos2 φ ψ s via the middle term.

Free choice theorems (general)

theorem ElliottSudo2025.fc_preconditions {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ ψ : BUSDen W E) (h : possible (φ ∨ᶠᶜ ψ) s) : (disjPos1 φ ψ s).Nonempty ∧ (disjPos2 φ ψ s).Nonempty

FC preconditions: if the modal disjunction is possible, both disjuncts contribute possibilities. (eq. 96)

theorem ElliottSudo2025.fc_disjPos1_nonempty {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ ψ : BUSDen W E) (h : possible (φ ∨ᶠᶜ ψ) s) : (disjPos1 φ ψ s).Nonempty

Extract disjPos1 nonemptiness from FC possibility.

theorem ElliottSudo2025.fc_disjPos2_nonempty {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ ψ : BUSDen W E) (h : possible (φ ∨ᶠᶜ ψ) s) : (disjPos2 φ ψ s).Nonempty

Extract disjPos2 nonemptiness from FC possibility.

Dual prohibition

theorem ElliottSudo2025.dual_prohibition_disjPos1 {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ ψ : BUSDen W E) (h : ¬(disjPos1 φ ψ s).Nonempty) : impossible (φ ∨ᶠᶜ ψ) s

Dual prohibition via disjPos1: if disjPos1 is empty (first disjunct contributes nothing), modal disjunction is impossible.

theorem ElliottSudo2025.dual_prohibition_disjPos2 {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ ψ : BUSDen W E) (h : ¬(disjPos2 φ ψ s).Nonempty) : impossible (φ ∨ᶠᶜ ψ) s

Dual prohibition via disjPos2: if disjPos2 is empty (second disjunct contributes nothing), modal disjunction is impossible.

Structural results (DNE, negation, binding)

theorem ElliottSudo2025.negation_swaps_dims {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (φ : BUSDen W E) : (~φ).positive s = φ.negative s ∧ (~φ).negative s = φ.positive s

In BUS, negation swaps positive and negative updates.

theorem ElliottSudo2025.exists_in_neg_dimension {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (x : ℕ) (φ : BUSDen W E) : (~(DynamicSemantics.BilateralDen.exists_ x φ)).negative s = (DynamicSemantics.BilateralDen.exists_ x φ).positive s

Negated existential has existential in negative dimension.

theorem ElliottSudo2025.dne_preserves_binding {W : Type u_1} {E : Type u_2} {s : Set (DynamicSemantics.Possibility W ℕ (Part E))} (x : ℕ) (φ ψ : BUSDen W E) : (~~(DynamicSemantics.BilateralDen.exists_ x φ) ⊙ ψ).positive s = (DynamicSemantics.BilateralDen.exists_ x φ ⊙ ψ).positive s

DNE preserves binding.

theorem ElliottSudo2025.dpl_diverges_on_double_negation {E : Type u_2} [Nontrivial E] : Examples.double_negation.judgment = Features.Judgment.acceptable ∧ ∃ (x : ℕ) (φ : DPL.Rel E), (DPL.Rel.exists_ x φ).neg.neg ≠ DPL.Rel.exists_ x φ

Divergence from DPL on doubly negated indefinites. The discourse Examples.double_negation ("It's not the case that John didn't see a bird. It was singing.") is judged acceptable; BUS derives the binding because ¬¬φ = φ (dne_preserves_binding), whereas in DPL negation is a test, so ¬¬∃xφ ≠ ∃xφ and the discourse referent never escapes.

Bathroom configuration

structure ElliottSudo2025.BathroomConfig (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

The bathroom disjunction configuration.

"Either there's no bathroom or it's in a funny place"

• bathroom : BUSDen W E

  The existential: ∃x.bathroom(x)

• funnyPlace : BUSDen W E

  The predicate on x: funny-place(x)

• x : ℕ

  The variable bound by the existential

def ElliottSudo2025.bathroomSentence {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) : BUSDen W E

The bathroom disjunction sentence: ¬∃x.bathroom(x) ∨ᶠᶜ funny-place(x)

Equations

• ElliottSudo2025.bathroomSentence cfg = ~cfg.bathroom ∨ᶠᶜ cfg.funnyPlace

Free choice with anaphora (bathroom-specific)

theorem ElliottSudo2025.anaphora_via_dne {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) : ~~cfg.bathroom = cfg.bathroom

DNE as structural equality: ¬¬φ = φ.

theorem ElliottSudo2025.fc_with_anaphora {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) (s : Set (DynamicSemantics.Possibility W ℕ (Part E))) (h_poss : possible (bathroomSentence cfg) s) (h_dp1 : disjPos1 (~cfg.bathroom) cfg.funnyPlace s ⊆ cfg.bathroom.negative s) (h_dp2 : disjPos2 (~cfg.bathroom) cfg.funnyPlace s ⊆ cfg.funnyPlace.positive (cfg.bathroom.positive s)) : (cfg.bathroom.negative s).Nonempty ∧ (cfg.funnyPlace.positive (cfg.bathroom.positive s)).Nonempty

FC with anaphora: the bathroom disjunction inference.

Eqs. 93-94 show that for bathroom disjunctions, the general disjPos1/disjPos2 (eq. 92) simplify so that:

• disjPos1 reduces to bath.negative s (possible there's no bathroom)
• disjPos2 reduces to funnyPlace.positive (bath.positive s) (possible there's a bathroom in a funny place)

The hypotheses h_dp1 and h_dp2 encode these simplifications: the general forms are contained in the simplified forms, so nonemptiness of the general forms transfers to the simplified forms.

The paper's partial-familiarity state (56)

[ES25a]'s (56): a state where x is defined at four possibilities and undefined at (w∅, []), so x is only partially familiar. The atomic sentence P(x) gaps at exactly the undefined possibility, so assertability (54) fails — the situation a uniform-base state cannot represent.

inductive ElliottSudo2025.PWorld : Type

• wa : PWorld
• wb : PWorld
• w0 : PWorld

@[instance_reducible]

instance ElliottSudo2025.instDecidableEqPWorld : DecidableEq PWorld

Equations

• ElliottSudo2025.instDecidableEqPWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ElliottSudo2025.PEntity : Type

• a : PEntity
• b : PEntity

@[instance_reducible]

instance ElliottSudo2025.instDecidableEqPEntity : DecidableEq PEntity

Equations

• ElliottSudo2025.instDecidableEqPEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ElliottSudo2025.pHolds : PEntity → PWorld → Prop

a is P at wa, b is P at wb, nothing is P at w0.

Equations

• ElliottSudo2025.pHolds ElliottSudo2025.PEntity.a ElliottSudo2025.PWorld.wa = True
• ElliottSudo2025.pHolds ElliottSudo2025.PEntity.b ElliottSudo2025.PWorld.wb = True
• ElliottSudo2025.pHolds x✝¹ x✝ = False

def ElliottSudo2025.xTo (e : PEntity) : ℕ → Part PEntity

The paper's [x → e]: register 0 defined, all else ∗.

Equations

• ElliottSudo2025.xTo e n = if n = 0 then Part.some e else ⊥

def ElliottSudo2025.blank : ℕ → Part PEntity

The paper's []: everything ∗.

Equations

• ElliottSudo2025.blank x✝ = ⊥

def ElliottSudo2025.s56 : Set (DynamicSemantics.Possibility PWorld ℕ (Part PEntity))

The state of (56).

Equations

• One or more equations did not get rendered due to their size.

theorem ElliottSudo2025.mem_positive_s56 : { world := PWorld.wa, assignment := xTo PEntity.a } ∈ (DynamicSemantics.BilateralDen.pred1 pHolds 0).positive s56

Positive consistency: (wa, [x → a]) survives assertion (56a).

theorem ElliottSudo2025.gap_mem_unknownUpdate_s56 : { world := PWorld.w0, assignment := blank } ∈ (DynamicSemantics.BilateralDen.pred1 pHolds 0).unknownUpdate s56

The gap: (w∅, []) subsists in neither dimension, so it is in the unknown update (56c).

theorem ElliottSudo2025.not_assertable_s56 : ¬(DynamicSemantics.BilateralDen.pred1 pHolds 0).assertable s56

(56)'s upshot: P(x) is not assertable at the partially familiar state.

theorem ElliottSudo2025.not_familiar_s56 : ¬DynamicSemantics.State.Familiar s56 0

x is not familiar at (56)'s state — familiarity fails, and by not_assertable_s56 so does assertability; the paper's point is that the converse can fail (assertability is strictly weaker).

Concrete example

inductive ElliottSudo2025.BathroomWorld : Type

• noBathroom : BathroomWorld
• bathroomNormal : BathroomWorld
• bathroomFunny : BathroomWorld

@[instance_reducible]

instance ElliottSudo2025.instDecidableEqBathroomWorld : DecidableEq BathroomWorld

Equations

• ElliottSudo2025.instDecidableEqBathroomWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ElliottSudo2025.instReprBathroomWorld : Repr BathroomWorld

Equations

• ElliottSudo2025.instReprBathroomWorld = { reprPrec := ElliottSudo2025.instReprBathroomWorld.repr }

def ElliottSudo2025.instReprBathroomWorld.repr : BathroomWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive ElliottSudo2025.BathroomEntity : Type

• theBathroom : BathroomEntity

@[instance_reducible]

instance ElliottSudo2025.instDecidableEqBathroomEntity : DecidableEq BathroomEntity

Equations

• ElliottSudo2025.instDecidableEqBathroomEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ElliottSudo2025.instReprBathroomEntity.repr : BathroomEntity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ElliottSudo2025.instReprBathroomEntity : Repr BathroomEntity

Equations

• ElliottSudo2025.instReprBathroomEntity = { reprPrec := ElliottSudo2025.instReprBathroomEntity.repr }

def ElliottSudo2025.isBathroom : BathroomEntity → BathroomWorld → Prop

Equations

• ElliottSudo2025.isBathroom ElliottSudo2025.BathroomEntity.theBathroom ElliottSudo2025.BathroomWorld.noBathroom = False
• ElliottSudo2025.isBathroom ElliottSudo2025.BathroomEntity.theBathroom x✝ = True

def ElliottSudo2025.inFunnyPlace : BathroomEntity → BathroomWorld → Prop

Equations

• ElliottSudo2025.inFunnyPlace ElliottSudo2025.BathroomEntity.theBathroom ElliottSudo2025.BathroomWorld.bathroomFunny = True
• ElliottSudo2025.inFunnyPlace x✝¹ x✝ = False

def ElliottSudo2025.exampleBathroomConfig : BathroomConfig BathroomWorld BathroomEntity

Equations

• One or more equations did not get rendered due to their size.