WALS Feature 136B: M in First Person Singular

@cite{wals-2013}

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

Chapter 136, 230 languages.

inductive Core.WALS.F136B.MInFirstPersonSingular : Type

WALS 136B values.

• noMInFirstPersonSingular : MInFirstPersonSingular
• mInFirstPersonSingular : MInFirstPersonSingular

instance Core.WALS.F136B.instDecidableEqMInFirstPersonSingular : DecidableEq MInFirstPersonSingular

Equations

• Core.WALS.F136B.instDecidableEqMInFirstPersonSingular x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.WALS.F136B.instBEqMInFirstPersonSingular.beq : MInFirstPersonSingular → MInFirstPersonSingular → Bool

Equations

• Core.WALS.F136B.instBEqMInFirstPersonSingular.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.WALS.F136B.instBEqMInFirstPersonSingular : BEq MInFirstPersonSingular

Equations

• Core.WALS.F136B.instBEqMInFirstPersonSingular = { beq := Core.WALS.F136B.instBEqMInFirstPersonSingular.beq }

instance Core.WALS.F136B.instReprMInFirstPersonSingular : Repr MInFirstPersonSingular

Equations

• Core.WALS.F136B.instReprMInFirstPersonSingular = { reprPrec := Core.WALS.F136B.instReprMInFirstPersonSingular.repr }

def Core.WALS.F136B.instReprMInFirstPersonSingular.repr : MInFirstPersonSingular → Nat → Std.Format

Equations

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

def Core.WALS.F136B.allData : List (Datapoint MInFirstPersonSingular)

Complete WALS 136B dataset (230 languages).

Equations

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

theorem Core.WALS.F136B.total_count : allData.length = 230

theorem Core.WALS.F136B.count_noMInFirstPersonSingular : (List.filter (fun (x : Datapoint MInFirstPersonSingular) => x.value == MInFirstPersonSingular.noMInFirstPersonSingular) allData).length = 177

theorem Core.WALS.F136B.count_mInFirstPersonSingular : (List.filter (fun (x : Datapoint MInFirstPersonSingular) => x.value == MInFirstPersonSingular.mInFirstPersonSingular) allData).length = 53

def Core.WALS.F136B.lookup (code : String) : Option (Datapoint MInFirstPersonSingular)

Look up a language by WALS code.

Equations

• Core.WALS.F136B.lookup code = Core.WALS.Datapoint.lookup Core.WALS.F136B.allData code

def Core.WALS.F136B.lookupISO (iso : String) : Option (Datapoint MInFirstPersonSingular)

Look up a language by ISO 639-3 code.

Equations

• Core.WALS.F136B.lookupISO iso = Core.WALS.Datapoint.lookupISO Core.WALS.F136B.allData iso