WALS Feature 137B: M in Second 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 137B.

Chapter 137, 230 languages.

inductive Core.WALS.F137B.MInSecondPersonSingular : Type

WALS 137B values.

• noMInSecondPersonSingular : MInSecondPersonSingular
• mInSecondPersonSingular : MInSecondPersonSingular

instance Core.WALS.F137B.instDecidableEqMInSecondPersonSingular : DecidableEq MInSecondPersonSingular

Equations

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

def Core.WALS.F137B.instBEqMInSecondPersonSingular.beq : MInSecondPersonSingular → MInSecondPersonSingular → Bool

Equations

• Core.WALS.F137B.instBEqMInSecondPersonSingular.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.WALS.F137B.instBEqMInSecondPersonSingular : BEq MInSecondPersonSingular

Equations

• Core.WALS.F137B.instBEqMInSecondPersonSingular = { beq := Core.WALS.F137B.instBEqMInSecondPersonSingular.beq }

instance Core.WALS.F137B.instReprMInSecondPersonSingular : Repr MInSecondPersonSingular

Equations

• Core.WALS.F137B.instReprMInSecondPersonSingular = { reprPrec := Core.WALS.F137B.instReprMInSecondPersonSingular.repr }

def Core.WALS.F137B.instReprMInSecondPersonSingular.repr : MInSecondPersonSingular → Nat → Std.Format

Equations

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

def Core.WALS.F137B.allData : List (Datapoint MInSecondPersonSingular)

Complete WALS 137B dataset (230 languages).

Equations

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

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

theorem Core.WALS.F137B.count_noMInSecondPersonSingular : (List.filter (fun (x : Datapoint MInSecondPersonSingular) => x.value == MInSecondPersonSingular.noMInSecondPersonSingular) allData).length = 152

theorem Core.WALS.F137B.count_mInSecondPersonSingular : (List.filter (fun (x : Datapoint MInSecondPersonSingular) => x.value == MInSecondPersonSingular.mInSecondPersonSingular) allData).length = 78

def Core.WALS.F137B.lookup (code : String) : Option (Datapoint MInSecondPersonSingular)

Look up a language by WALS code.

Equations

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

def Core.WALS.F137B.lookupISO (iso : String) : Option (Datapoint MInSecondPersonSingular)

Look up a language by ISO 639-3 code.

Equations

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