WALS Feature 116A: Polar Questions

@cite{dryer-2013-wals}

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

Chapter 116, 955 languages.

inductive Core.WALS.F116A.PolarQuestionType : Type

WALS 116A values.

• questionParticle : PolarQuestionType
• interrogativeVerbMorphology : PolarQuestionType
• mixtureOfPreviousTwoTypes : PolarQuestionType
• interrogativeWordOrder : PolarQuestionType
• absenceOfDeclarativeMorphemes : PolarQuestionType
• interrogativeIntonationOnly : PolarQuestionType
• noInterrogativeDeclarativeDistinction : PolarQuestionType

instance Core.WALS.F116A.instDecidableEqPolarQuestionType : DecidableEq PolarQuestionType

Equations

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

instance Core.WALS.F116A.instBEqPolarQuestionType : BEq PolarQuestionType

Equations

• Core.WALS.F116A.instBEqPolarQuestionType = { beq := Core.WALS.F116A.instBEqPolarQuestionType.beq }

def Core.WALS.F116A.instBEqPolarQuestionType.beq : PolarQuestionType → PolarQuestionType → Bool

Equations

• Core.WALS.F116A.instBEqPolarQuestionType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.WALS.F116A.instReprPolarQuestionType.repr : PolarQuestionType → Nat → Std.Format

Equations

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

instance Core.WALS.F116A.instReprPolarQuestionType : Repr PolarQuestionType

Equations

• Core.WALS.F116A.instReprPolarQuestionType = { reprPrec := Core.WALS.F116A.instReprPolarQuestionType.repr }

def Core.WALS.F116A.allData : List (Datapoint PolarQuestionType)

Complete WALS 116A dataset (955 languages).

Equations

• Core.WALS.F116A.allData = Core.WALS.F116A.allData_0✝ ++ Core.WALS.F116A.allData_1✝

theorem Core.WALS.F116A.total_count : allData.length = 955

theorem Core.WALS.F116A.count_questionParticle : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.questionParticle) allData).length = 585

theorem Core.WALS.F116A.count_interrogativeVerbMorphology : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.interrogativeVerbMorphology) allData).length = 164

theorem Core.WALS.F116A.count_mixtureOfPreviousTwoTypes : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.mixtureOfPreviousTwoTypes) allData).length = 15

theorem Core.WALS.F116A.count_interrogativeWordOrder : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.interrogativeWordOrder) allData).length = 13

theorem Core.WALS.F116A.count_absenceOfDeclarativeMorphemes : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.absenceOfDeclarativeMorphemes) allData).length = 4

theorem Core.WALS.F116A.count_interrogativeIntonationOnly : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.interrogativeIntonationOnly) allData).length = 173

theorem Core.WALS.F116A.count_noInterrogativeDeclarativeDistinction : (List.filter (fun (x : Datapoint PolarQuestionType) => x.value == PolarQuestionType.noInterrogativeDeclarativeDistinction) allData).length = 1

def Core.WALS.F116A.lookup (code : String) : Option (Datapoint PolarQuestionType)

Look up a language by WALS code.

Equations

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

def Core.WALS.F116A.lookupISO (iso : String) : Option (Datapoint PolarQuestionType)

Look up a language by ISO 639-3 code.

Equations

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