WALS Feature 53A: Ordinal Numerals

@cite{wals-2013}

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

Chapter 53, 321 languages.

inductive Data.WALS.F53A.OrdinalNumerals : Type

WALS 53A values.

• none : OrdinalNumerals

  None (33 languages).

• oneTwoThree : OrdinalNumerals

  One, two, three (3 languages).

• firstTwoThree : OrdinalNumerals

  First, two, three (12 languages).

• oneThTwoThThreeTh : OrdinalNumerals

  One-th, two-th, three-th (41 languages).

• firstOneThTwoThThreeTh : OrdinalNumerals

  First/one-th, two-th, three-th (54 languages).

• firstTwoThThreeTh : OrdinalNumerals

  First, two-th, three-th (110 languages).

• firstSecondThreeTh : OrdinalNumerals

  First, second, three-th (61 languages).

• various : OrdinalNumerals

  Various (7 languages).

@[implicit_reducible]

instance Data.WALS.F53A.instDecidableEqOrdinalNumerals : DecidableEq OrdinalNumerals

Equations

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

def Data.WALS.F53A.instBEqOrdinalNumerals.beq : OrdinalNumerals → OrdinalNumerals → Bool

Equations

• Data.WALS.F53A.instBEqOrdinalNumerals.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Data.WALS.F53A.instBEqOrdinalNumerals : BEq OrdinalNumerals

Equations

• Data.WALS.F53A.instBEqOrdinalNumerals = { beq := Data.WALS.F53A.instBEqOrdinalNumerals.beq }

@[implicit_reducible]

instance Data.WALS.F53A.instReprOrdinalNumerals : Repr OrdinalNumerals

Equations

• Data.WALS.F53A.instReprOrdinalNumerals = { reprPrec := Data.WALS.F53A.instReprOrdinalNumerals.repr }

def Data.WALS.F53A.instReprOrdinalNumerals.repr : OrdinalNumerals → Nat → Std.Format

Equations

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

def Data.WALS.F53A.allData : List (Datapoint OrdinalNumerals)

Complete WALS 53A dataset (321 languages).

Equations

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

def Data.WALS.F53A.lookup (code : String) : Option (Datapoint OrdinalNumerals)

Look up a language by WALS code.

Equations

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

def Data.WALS.F53A.lookupISO (iso : String) : Option (Datapoint OrdinalNumerals)

Look up a language by ISO 639-3 code.

Equations

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