WALS Feature 144P: NegSOV Order

@cite{wals-2013}

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

Chapter 144, 408 languages.

inductive Data.WALS.F144P.NegsovOrder : Type

WALS 144P values.

• nodoubleneg : NegsovOrder

  NoDoubleNeg (18 languages).

• optdoubleneg : NegsovOrder

  OptDoubleNeg (1 languages).

• onlywithanotherneg : NegsovOrder

  OnlyWithAnotherNeg (8 languages).

• noNegsov : NegsovOrder

  No NegSOV (381 languages).

@[implicit_reducible]

instance Data.WALS.F144P.instDecidableEqNegsovOrder : DecidableEq NegsovOrder

Equations

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

@[implicit_reducible]

instance Data.WALS.F144P.instBEqNegsovOrder : BEq NegsovOrder

Equations

• Data.WALS.F144P.instBEqNegsovOrder = { beq := Data.WALS.F144P.instBEqNegsovOrder.beq }

def Data.WALS.F144P.instBEqNegsovOrder.beq : NegsovOrder → NegsovOrder → Bool

Equations

• Data.WALS.F144P.instBEqNegsovOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Data.WALS.F144P.instReprNegsovOrder : Repr NegsovOrder

Equations

• Data.WALS.F144P.instReprNegsovOrder = { reprPrec := Data.WALS.F144P.instReprNegsovOrder.repr }

def Data.WALS.F144P.instReprNegsovOrder.repr : NegsovOrder → Nat → Std.Format

Equations

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

def Data.WALS.F144P.allData : List (Datapoint NegsovOrder)

Complete WALS 144P dataset (408 languages).

Equations

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

def Data.WALS.F144P.lookup (code : String) : Option (Datapoint NegsovOrder)

Look up a language by WALS code.

Equations

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

def Data.WALS.F144P.lookupISO (iso : String) : Option (Datapoint NegsovOrder)

Look up a language by ISO 639-3 code.

Equations

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