WALS Feature 139A: Irregular Negatives in Sign Languages

@cite{wals-2013}

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

Chapter 139, 35 languages.

inductive Data.WALS.F139A.IrregularNegativesInSignLanguages : Type

WALS 139A values.

• none : IrregularNegativesInSignLanguages

  None (1 languages).

• one : IrregularNegativesInSignLanguages

  One (3 languages).

• some : IrregularNegativesInSignLanguages

  Some (2-5) (10 languages).

• many : IrregularNegativesInSignLanguages

  Many (more than 5) (21 languages).

@[implicit_reducible]

instance Data.WALS.F139A.instDecidableEqIrregularNegativesInSignLanguages : DecidableEq IrregularNegativesInSignLanguages

Equations

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

def Data.WALS.F139A.instBEqIrregularNegativesInSignLanguages.beq : IrregularNegativesInSignLanguages → IrregularNegativesInSignLanguages → Bool

Equations

• Data.WALS.F139A.instBEqIrregularNegativesInSignLanguages.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Data.WALS.F139A.instBEqIrregularNegativesInSignLanguages : BEq IrregularNegativesInSignLanguages

Equations

• Data.WALS.F139A.instBEqIrregularNegativesInSignLanguages = { beq := Data.WALS.F139A.instBEqIrregularNegativesInSignLanguages.beq }

@[implicit_reducible]

instance Data.WALS.F139A.instReprIrregularNegativesInSignLanguages : Repr IrregularNegativesInSignLanguages

Equations

• Data.WALS.F139A.instReprIrregularNegativesInSignLanguages = { reprPrec := Data.WALS.F139A.instReprIrregularNegativesInSignLanguages.repr }

def Data.WALS.F139A.instReprIrregularNegativesInSignLanguages.repr : IrregularNegativesInSignLanguages → Nat → Std.Format

Equations

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

def Data.WALS.F139A.allData : List (Datapoint IrregularNegativesInSignLanguages)

Complete WALS 139A dataset (35 languages).

Equations

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

def Data.WALS.F139A.lookup (code : String) : Option (Datapoint IrregularNegativesInSignLanguages)

Look up a language by WALS code.

Equations

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

def Data.WALS.F139A.lookupISO (iso : String) : Option (Datapoint IrregularNegativesInSignLanguages)

Look up a language by ISO 639-3 code.

Equations

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