Focus marking

Binary focus marking (Mark): the marking feature of the focus axis, one of [Kri08]'s four information-structure notions. Use Mark when only the binary focused-vs-not distinction is needed; Alternatives.AltMeaning carries the Roothian alternative-set structure.

inductive Focus.Mark : Type

Binary focus marking — whether a constituent bears focus (pitch accent / contrast) or not.

• focused : Mark

  Constituent is focus-marked (pitch accent / contrast).

• nonFocused : Mark

  Constituent is not focus-marked.

@[instance_reducible]

instance Focus.instDecidableEqMark : DecidableEq Mark

Equations

• Focus.instDecidableEqMark x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Focus.instReprMark.repr : Mark → Nat → Std.Format

Equations

• Focus.instReprMark.repr Focus.Mark.focused prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Mark.focused")).group prec✝
• Focus.instReprMark.repr Focus.Mark.nonFocused prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Mark.nonFocused")).group prec✝

@[instance_reducible]

instance Focus.instReprMark : Repr Mark

Equations

• Focus.instReprMark = { reprPrec := Focus.instReprMark.repr }