WALS Feature 143B: Obligatory Double Negation

@cite{wals-2013}

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

Chapter 143, 119 languages.

inductive Data.WALS.F143B.ObligatoryDoubleNegation : Type

WALS 143B values.

• negvneg : ObligatoryDoubleNegation

  NegVNeg (35 languages).

• negVNeg : ObligatoryDoubleNegation

  Neg[V-Neg] (28 languages).

• negVNeg_3 : ObligatoryDoubleNegation

  [Neg-V]Neg (9 languages).

• negVNeg_4 : ObligatoryDoubleNegation

  [Neg-V-Neg] (27 languages).

• negativeToneVneg : ObligatoryDoubleNegation

  Negative tone & VNeg (1 languages).

• negativeToneNegV : ObligatoryDoubleNegation

  Negative tone & [Neg-V] (2 languages).

• negnegv : ObligatoryDoubleNegation

  NegNegV (2 languages).

• negNegV : ObligatoryDoubleNegation

  Neg[Neg-V] (2 languages).

• vnegneg : ObligatoryDoubleNegation

  VNegNeg (2 languages).

• type1Type2 : ObligatoryDoubleNegation

  Type 1 / Type 2 (1 languages).

• type1Type3 : ObligatoryDoubleNegation

  Type 1 / Type 3 (1 languages).

• type1Type5 : ObligatoryDoubleNegation

  Type 1 / Type 5 (1 languages).

• type1Type7 : ObligatoryDoubleNegation

  Type 1 / Type 7 (1 languages).

• type1Type9 : ObligatoryDoubleNegation

  Type 1 / Type 9 (1 languages).

• type2Type4 : ObligatoryDoubleNegation

  Type 2 / Type 4 (1 languages).

• obligdoublenegOpttripleneg : ObligatoryDoubleNegation

  ObligDoubleNeg&OptTripleNeg (5 languages).

@[implicit_reducible]

instance Data.WALS.F143B.instDecidableEqObligatoryDoubleNegation : DecidableEq ObligatoryDoubleNegation

Equations

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

def Data.WALS.F143B.instBEqObligatoryDoubleNegation.beq : ObligatoryDoubleNegation → ObligatoryDoubleNegation → Bool

Equations

• Data.WALS.F143B.instBEqObligatoryDoubleNegation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Data.WALS.F143B.instBEqObligatoryDoubleNegation : BEq ObligatoryDoubleNegation

Equations

• Data.WALS.F143B.instBEqObligatoryDoubleNegation = { beq := Data.WALS.F143B.instBEqObligatoryDoubleNegation.beq }

def Data.WALS.F143B.instReprObligatoryDoubleNegation.repr : ObligatoryDoubleNegation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.WALS.F143B.instReprObligatoryDoubleNegation : Repr ObligatoryDoubleNegation

Equations

• Data.WALS.F143B.instReprObligatoryDoubleNegation = { reprPrec := Data.WALS.F143B.instReprObligatoryDoubleNegation.repr }

def Data.WALS.F143B.allData : List (Datapoint ObligatoryDoubleNegation)

Complete WALS 143B dataset (119 languages).

Equations

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

def Data.WALS.F143B.lookup (code : String) : Option (Datapoint ObligatoryDoubleNegation)

Look up a language by WALS code.

Equations

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

def Data.WALS.F143B.lookupISO (iso : String) : Option (Datapoint ObligatoryDoubleNegation)

Look up a language by ISO 639-3 code.

Equations

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