The sibilant-harmony tier alphabet

The minimal segment alphabet shared by sibilant-harmony phonotactics: an anterior class ([s, z, ts, …]), a posterior (postalveolar) class ([ʃ, ʒ, tʃ, …]), and a neutral class for everything off the harmony tier. Sibilant.onTier is the tier- membership predicate the subregular harmony grammars project on.

Substrate only: a study of a particular system supplies its own forbidden-pair relation over this alphabet — symmetric (TSLGrammar.agree) or asymmetric (TSLGrammar.ofForbiddenPairs) — and keeps its language-specific data and citations.

inductive Subregular.Sibilant : Type

The three sibilant-harmony classes: anterior (s-class), posterior (ʃ-class), and neutral (off the harmony tier).

• anterior : Sibilant
• posterior : Sibilant
• neutral : Sibilant

@[implicit_reducible]

instance Subregular.instDecidableEqSibilant : DecidableEq Sibilant

Equations

• Subregular.instDecidableEqSibilant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Subregular.instReprSibilant.repr : Sibilant → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Subregular.instReprSibilant : Repr Sibilant

Equations

• Subregular.instReprSibilant = { reprPrec := Subregular.instReprSibilant.repr }

@[reducible]

def Subregular.Sibilant.onTier : Sibilant → Prop

The harmony-tier predicate: sibilants project, neutral material is transparent.

Equations

• Subregular.Sibilant.anterior.onTier = True
• Subregular.Sibilant.posterior.onTier = True
• Subregular.Sibilant.neutral.onTier = False

@[implicit_reducible]

instance Subregular.instDecidablePredSibilantOnTier : DecidablePred Sibilant.onTier

Equations

• Subregular.instDecidablePredSibilantOnTier Subregular.Sibilant.anterior = isTrue trivial
• Subregular.instDecidablePredSibilantOnTier Subregular.Sibilant.posterior = isTrue trivial
• Subregular.instDecidablePredSibilantOnTier Subregular.Sibilant.neutral = isFalse not_false