Hiatus resolution samples: schema

Typed schema for a paper's report of which vowel elides where two vowels meet: for each language the paper reports on, the kind of juncture and the vowel that elides there. Generated rows live in Data/Hiatus/<Paper>.lean, emitted from the canonical <Paper>.json by scripts/gen_hiatus.py.

This is data: it imports nothing from Linglib/ and states no theorems. A language appears once for each juncture and elided vowel the paper reports for it, so a language that elides the first vowel with some suffixes and the second with others has two rows.

References

• [Cas97]
• [Mko21]

inductive Data.Hiatus.Juncture : Type

The kind of juncture at which two vowels meet.

• lexicalLexical : Juncture

  Between two lexical words.

• lexicalFunction : Juncture

  Between a lexical word and a following function word.

• prefixRoot : Juncture

  Between a prefix of at least a consonant and a vowel and a root.

• rootSuffix : Juncture

  Between a root and a suffix.

• suffixSuffix : Juncture

  Between two suffixes.

• cliticClitic : Juncture

  Between two enclitics.

@[instance_reducible]

instance Data.Hiatus.instDecidableEqJuncture : DecidableEq Juncture

Equations

• Data.Hiatus.instDecidableEqJuncture x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.Hiatus.instReprJuncture.repr : Juncture → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.Hiatus.instReprJuncture : Repr Juncture

Equations

• Data.Hiatus.instReprJuncture = { reprPrec := Data.Hiatus.instReprJuncture.repr }

@[instance_reducible]

instance Data.Hiatus.instFintypeJuncture : Fintype Juncture

Equations

• Data.Hiatus.instFintypeJuncture = { elems := { val := ↑Data.Hiatus.Juncture.enumList, nodup := Data.Hiatus.Juncture.enumList_nodup }, complete := Data.Hiatus.instFintypeJuncture._proof_1 }

inductive Data.Hiatus.ElidedVowel : Type

The vowel that elides, the first or the second of the two.

• first : ElidedVowel
• second : ElidedVowel

@[instance_reducible]

instance Data.Hiatus.instDecidableEqElidedVowel : DecidableEq ElidedVowel

Equations

• Data.Hiatus.instDecidableEqElidedVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.Hiatus.instReprElidedVowel.repr : ElidedVowel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.Hiatus.instReprElidedVowel : Repr ElidedVowel

Equations

• Data.Hiatus.instReprElidedVowel = { reprPrec := Data.Hiatus.instReprElidedVowel.repr }

@[instance_reducible]

instance Data.Hiatus.instFintypeElidedVowel : Fintype ElidedVowel

Equations

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

structure Data.Hiatus.ElisionRow : Type

A language's elision at a kind of juncture, as a paper reports it.

• language : String

  The language, under the name the paper uses.

• juncture : Juncture

  The kind of juncture.

• elided : ElidedVowel

  The vowel that elides there.

• tentative : Bool

  The paper marks the report as uncertain.

def Data.Hiatus.instDecidableEqElisionRow.decEq (x✝ x✝¹ : ElisionRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.Hiatus.instDecidableEqElisionRow : DecidableEq ElisionRow

Equations

• Data.Hiatus.instDecidableEqElisionRow = Data.Hiatus.instDecidableEqElisionRow.decEq

def Data.Hiatus.instReprElisionRow.repr : ElisionRow → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.Hiatus.instReprElisionRow : Repr ElisionRow

Equations

• Data.Hiatus.instReprElisionRow = { reprPrec := Data.Hiatus.instReprElisionRow.repr }