WALS Feature 17A: Rhythm Types

@cite{wals-2013}

Auto-generated from WALS v2020.4 CLDF data. Do not edit by hand — regenerate with python3 scripts/gen_wals.py 17A.

Chapter 17, 323 languages.

inductive Data.WALS.F17A.RhythmTypes : Type

WALS 17A values.

• trochaic : RhythmTypes

  Trochaic (153 languages).

• iambic : RhythmTypes

  Iambic (31 languages).

• dualBothTrochaicAndIambic : RhythmTypes

  Dual: both trochaic and iambic (4 languages).

• undetermined : RhythmTypes

  Undetermined (37 languages).

• noRhythmicStress : RhythmTypes

  No rhythmic stress (98 languages).

@[implicit_reducible]

instance Data.WALS.F17A.instDecidableEqRhythmTypes : DecidableEq RhythmTypes

Equations

• Data.WALS.F17A.instDecidableEqRhythmTypes x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Data.WALS.F17A.instBEqRhythmTypes : BEq RhythmTypes

Equations

• Data.WALS.F17A.instBEqRhythmTypes = { beq := Data.WALS.F17A.instBEqRhythmTypes.beq }

def Data.WALS.F17A.instBEqRhythmTypes.beq : RhythmTypes → RhythmTypes → Bool

Equations

• Data.WALS.F17A.instBEqRhythmTypes.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Data.WALS.F17A.instReprRhythmTypes.repr : RhythmTypes → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.WALS.F17A.instReprRhythmTypes : Repr RhythmTypes

Equations

• Data.WALS.F17A.instReprRhythmTypes = { reprPrec := Data.WALS.F17A.instReprRhythmTypes.repr }

def Data.WALS.F17A.allData : List (Datapoint RhythmTypes)

Complete WALS 17A dataset (323 languages).

Equations

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

def Data.WALS.F17A.lookup (code : String) : Option (Datapoint RhythmTypes)

Look up a language by WALS code.

Equations

• Data.WALS.F17A.lookup code = Data.WALS.Datapoint.lookup Data.WALS.F17A.allData code

def Data.WALS.F17A.lookupISO (iso : String) : Option (Datapoint RhythmTypes)

Look up a language by ISO 639-3 code.

Equations

• Data.WALS.F17A.lookupISO iso = Data.WALS.Datapoint.lookupISO Data.WALS.F17A.allData iso