WALS Feature 125A: Purpose Clauses

@cite{cristofaro-2013}

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

Chapter 125, 170 languages.

inductive Data.WALS.F125A.PurposeClauseType : Type

WALS 125A values.

• balanced : PurposeClauseType

  Balanced (38 languages).

• balancedDeranked : PurposeClauseType

  Balanced/deranked (30 languages).

• deranked : PurposeClauseType

  Deranked (102 languages).

@[implicit_reducible]

instance Data.WALS.F125A.instDecidableEqPurposeClauseType : DecidableEq PurposeClauseType

Equations

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

@[implicit_reducible]

instance Data.WALS.F125A.instBEqPurposeClauseType : BEq PurposeClauseType

Equations

• Data.WALS.F125A.instBEqPurposeClauseType = { beq := Data.WALS.F125A.instBEqPurposeClauseType.beq }

def Data.WALS.F125A.instBEqPurposeClauseType.beq : PurposeClauseType → PurposeClauseType → Bool

Equations

• Data.WALS.F125A.instBEqPurposeClauseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Data.WALS.F125A.instReprPurposeClauseType.repr : PurposeClauseType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.WALS.F125A.instReprPurposeClauseType : Repr PurposeClauseType

Equations

• Data.WALS.F125A.instReprPurposeClauseType = { reprPrec := Data.WALS.F125A.instReprPurposeClauseType.repr }

def Data.WALS.F125A.allData : List (Datapoint PurposeClauseType)

Complete WALS 125A dataset (170 languages).

Equations

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

def Data.WALS.F125A.lookup (code : String) : Option (Datapoint PurposeClauseType)

Look up a language by WALS code.

Equations

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

def Data.WALS.F125A.lookupISO (iso : String) : Option (Datapoint PurposeClauseType)

Look up a language by ISO 639-3 code.

Equations

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