WALS Feature 144C: Languages with different word order in negative clauses

@cite{wals-2013}

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

Chapter 144, 28 languages.

inductive Core.WALS.F144C.LanguagesWithDifferentWordOrderInNegativeClauses : Type

WALS 144C values.

• vsoButNegsvo : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButSnegov : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButSonegv : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButSovneg : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButNegvso : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButSoVNeg : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButSoNegV : LanguagesWithDifferentWordOrderInNegativeClauses
• osvButNegsvoONegVS : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButNegsnegov : LanguagesWithDifferentWordOrderInNegativeClauses
• svoButSonegVNegSoNegVNeg : LanguagesWithDifferentWordOrderInNegativeClauses
• sovButSonegVNegSNegVNegO : LanguagesWithDifferentWordOrderInNegativeClauses
• svoVsoButNegsvoneg : LanguagesWithDifferentWordOrderInNegativeClauses
• svoVsoButNegVSo : LanguagesWithDifferentWordOrderInNegativeClauses
• svoSovButSvoneg : LanguagesWithDifferentWordOrderInNegativeClauses
• svoSovButSnegvo : LanguagesWithDifferentWordOrderInNegativeClauses
• svoSovButSnegov : LanguagesWithDifferentWordOrderInNegativeClauses
• svoSovButSovneg : LanguagesWithDifferentWordOrderInNegativeClauses

instance Core.WALS.F144C.instDecidableEqLanguagesWithDifferentWordOrderInNegativeClauses : DecidableEq LanguagesWithDifferentWordOrderInNegativeClauses

Equations

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

def Core.WALS.F144C.instBEqLanguagesWithDifferentWordOrderInNegativeClauses.beq : LanguagesWithDifferentWordOrderInNegativeClauses → LanguagesWithDifferentWordOrderInNegativeClauses → Bool

Equations

• Core.WALS.F144C.instBEqLanguagesWithDifferentWordOrderInNegativeClauses.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.WALS.F144C.instBEqLanguagesWithDifferentWordOrderInNegativeClauses : BEq LanguagesWithDifferentWordOrderInNegativeClauses

Equations

• Core.WALS.F144C.instBEqLanguagesWithDifferentWordOrderInNegativeClauses = { beq := Core.WALS.F144C.instBEqLanguagesWithDifferentWordOrderInNegativeClauses.beq }

def Core.WALS.F144C.instReprLanguagesWithDifferentWordOrderInNegativeClauses.repr : LanguagesWithDifferentWordOrderInNegativeClauses → Nat → Std.Format

Equations

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

instance Core.WALS.F144C.instReprLanguagesWithDifferentWordOrderInNegativeClauses : Repr LanguagesWithDifferentWordOrderInNegativeClauses

Equations

• Core.WALS.F144C.instReprLanguagesWithDifferentWordOrderInNegativeClauses = { reprPrec := Core.WALS.F144C.instReprLanguagesWithDifferentWordOrderInNegativeClauses.repr }

def Core.WALS.F144C.allData : List (Datapoint LanguagesWithDifferentWordOrderInNegativeClauses)

Complete WALS 144C dataset (28 languages).

Equations

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

theorem Core.WALS.F144C.total_count : allData.length = 28

theorem Core.WALS.F144C.count_vsoButNegsvo : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.vsoButNegsvo) allData).length = 6

theorem Core.WALS.F144C.count_svoButSnegov : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButSnegov) allData).length = 3

theorem Core.WALS.F144C.count_svoButSonegv : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButSonegv) allData).length = 1

theorem Core.WALS.F144C.count_svoButSovneg : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButSovneg) allData).length = 1

theorem Core.WALS.F144C.count_svoButNegvso : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButNegvso) allData).length = 1

theorem Core.WALS.F144C.count_svoButSoVNeg : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButSoVNeg) allData).length = 1

theorem Core.WALS.F144C.count_svoButSoNegV : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButSoNegV) allData).length = 1

theorem Core.WALS.F144C.count_osvButNegsvoONegVS : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.osvButNegsvoONegVS) allData).length = 1

theorem Core.WALS.F144C.count_svoButNegsnegov : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButNegsnegov) allData).length = 1

theorem Core.WALS.F144C.count_svoButSonegVNegSoNegVNeg : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoButSonegVNegSoNegVNeg) allData).length = 1

theorem Core.WALS.F144C.count_sovButSonegVNegSNegVNegO : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.sovButSonegVNegSNegVNegO) allData).length = 1

theorem Core.WALS.F144C.count_svoVsoButNegsvoneg : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoVsoButNegsvoneg) allData).length = 1

theorem Core.WALS.F144C.count_svoVsoButNegVSo : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoVsoButNegVSo) allData).length = 1

theorem Core.WALS.F144C.count_svoSovButSvoneg : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoSovButSvoneg) allData).length = 5

theorem Core.WALS.F144C.count_svoSovButSnegvo : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoSovButSnegvo) allData).length = 1

theorem Core.WALS.F144C.count_svoSovButSnegov : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoSovButSnegov) allData).length = 1

theorem Core.WALS.F144C.count_svoSovButSovneg : (List.filter (fun (x : Datapoint LanguagesWithDifferentWordOrderInNegativeClauses) => x.value == LanguagesWithDifferentWordOrderInNegativeClauses.svoSovButSovneg) allData).length = 1

def Core.WALS.F144C.lookup (code : String) : Option (Datapoint LanguagesWithDifferentWordOrderInNegativeClauses)

Look up a language by WALS code.

Equations

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

def Core.WALS.F144C.lookupISO (iso : String) : Option (Datapoint LanguagesWithDifferentWordOrderInNegativeClauses)

Look up a language by ISO 639-3 code.

Equations

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