inductive Core.Prosody.PitchAccent : Type

Pitch accent types (@cite{pierrehumbert-1980}, ToBI conventions).

Pitch accents mark focus/contrast at the word level:

• H*: Sharp rise, typically marks rheme focus ("the BEANS")
• L+H*: Rise from low, typically marks theme focus ("FRED ate")
• null: No accent (background material)

• H_star : PitchAccent
• L_plus_H_star : PitchAccent
• null : PitchAccent

def Core.Prosody.instReprPitchAccent.repr : PitchAccent → Nat → Std.Format

Equations

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

instance Core.Prosody.instReprPitchAccent : Repr PitchAccent

Equations

• Core.Prosody.instReprPitchAccent = { reprPrec := Core.Prosody.instReprPitchAccent.repr }

instance Core.Prosody.instDecidableEqPitchAccent : DecidableEq PitchAccent

Equations

• Core.Prosody.instDecidableEqPitchAccent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Prosody.instInhabitedPitchAccent : Inhabited PitchAccent

Equations

• Core.Prosody.instInhabitedPitchAccent = { default := Core.Prosody.instInhabitedPitchAccent.default }

def Core.Prosody.instInhabitedPitchAccent.default : PitchAccent

Equations

• Core.Prosody.instInhabitedPitchAccent.default = Core.Prosody.PitchAccent.H_star

instance Core.Prosody.instBEqPitchAccent : BEq PitchAccent

Equations

• Core.Prosody.instBEqPitchAccent = { beq := Core.Prosody.instBEqPitchAccent.beq }

def Core.Prosody.instBEqPitchAccent.beq : PitchAccent → PitchAccent → Bool

Equations

• Core.Prosody.instBEqPitchAccent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Core.Prosody.BoundaryTone : Type

Boundary tones mark prosodic phrase edges.

Following @cite{pierrehumbert-1980} and @cite{beckman-pierrehumbert-1986}:

• L: Low intermediate phrase boundary
• LH%: Rising intonational phrase boundary (continuation)
• LL%: Falling intonational phrase boundary (finality)

• L : BoundaryTone
• LH_pct : BoundaryTone
• LL_pct : BoundaryTone

instance Core.Prosody.instReprBoundaryTone : Repr BoundaryTone

Equations

• Core.Prosody.instReprBoundaryTone = { reprPrec := Core.Prosody.instReprBoundaryTone.repr }

def Core.Prosody.instReprBoundaryTone.repr : BoundaryTone → Nat → Std.Format

Equations

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

instance Core.Prosody.instDecidableEqBoundaryTone : DecidableEq BoundaryTone

Equations

• Core.Prosody.instDecidableEqBoundaryTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Prosody.instInhabitedBoundaryTone : Inhabited BoundaryTone

Equations

• Core.Prosody.instInhabitedBoundaryTone = { default := Core.Prosody.instInhabitedBoundaryTone.default }

def Core.Prosody.instInhabitedBoundaryTone.default : BoundaryTone

Equations

• Core.Prosody.instInhabitedBoundaryTone.default = Core.Prosody.BoundaryTone.L

instance Core.Prosody.instBEqBoundaryTone : BEq BoundaryTone

Equations

• Core.Prosody.instBEqBoundaryTone = { beq := Core.Prosody.instBEqBoundaryTone.beq }

def Core.Prosody.instBEqBoundaryTone.beq : BoundaryTone → BoundaryTone → Bool

Equations

• Core.Prosody.instBEqBoundaryTone.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Core.Prosody.ProsodicLevel : Type

Prosodic hierarchy levels.

σ < f < ω < φ < ι

Used by @cite{kratzer-selkirk-2020} spellout constraints.

• σ : ProsodicLevel
• f : ProsodicLevel
• ω : ProsodicLevel
• φ : ProsodicLevel
• ι : ProsodicLevel

instance Core.Prosody.instDecidableEqProsodicLevel : DecidableEq ProsodicLevel

Equations

• Core.Prosody.instDecidableEqProsodicLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Prosody.instReprProsodicLevel : Repr ProsodicLevel

Equations

• Core.Prosody.instReprProsodicLevel = { reprPrec := Core.Prosody.instReprProsodicLevel.repr }

def Core.Prosody.instReprProsodicLevel.repr : ProsodicLevel → Nat → Std.Format

Equations

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

instance Core.Prosody.instBEqProsodicLevel : BEq ProsodicLevel

Equations

• Core.Prosody.instBEqProsodicLevel = { beq := Core.Prosody.instBEqProsodicLevel.beq }

def Core.Prosody.instBEqProsodicLevel.beq : ProsodicLevel → ProsodicLevel → Bool

Equations

• Core.Prosody.instBEqProsodicLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Prosody.instOrdProsodicLevel : Ord ProsodicLevel

Equations

• Core.Prosody.instOrdProsodicLevel = { compare := Core.Prosody.instOrdProsodicLevel.ord }

def Core.Prosody.instOrdProsodicLevel.ord : ProsodicLevel → ProsodicLevel → Ordering

Equations

• Core.Prosody.instOrdProsodicLevel.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

instance Core.Prosody.instLTProsodicLevel : LT ProsodicLevel

Equations

• Core.Prosody.instLTProsodicLevel = { lt := fun (a b : Core.Prosody.ProsodicLevel) => a.ctorIdx < b.ctorIdx }

instance Core.Prosody.instLEProsodicLevel : LE ProsodicLevel

Equations

• Core.Prosody.instLEProsodicLevel = { le := fun (a b : Core.Prosody.ProsodicLevel) => a.ctorIdx ≤ b.ctorIdx }

structure Core.Prosody.ProsodicConstituent : Type

Head-prominence: each prosodic constituent has exactly one prominent daughter (its head). K&S (32).

• level : ProsodicLevel
• isHead : Bool

  Whether this constituent is the head (most prominent) of its parent

def Core.Prosody.instReprProsodicConstituent.repr : ProsodicConstituent → Nat → Std.Format

Equations

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

instance Core.Prosody.instReprProsodicConstituent : Repr ProsodicConstituent

Equations

• Core.Prosody.instReprProsodicConstituent = { reprPrec := Core.Prosody.instReprProsodicConstituent.repr }