WALS Feature 90E: Correlative relative clauses

@cite{wals-2013}

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

Chapter 90, 23 languages.

inductive Core.WALS.F90E.CorrelativeRelativeClauses : Type

WALS 90E values.

• correlativeRelativeClauseDominant : CorrelativeRelativeClauses
• correlativeOrReln : CorrelativeRelativeClauses
• correlativeOrNrel : CorrelativeRelativeClauses
• correlativeOrInternallyHeaded : CorrelativeRelativeClauses
• correlativeOrAdjoined : CorrelativeRelativeClauses
• correlativeAsNondominantType : CorrelativeRelativeClauses
• correlativeExists : CorrelativeRelativeClauses

instance Core.WALS.F90E.instDecidableEqCorrelativeRelativeClauses : DecidableEq CorrelativeRelativeClauses

Equations

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

def Core.WALS.F90E.instBEqCorrelativeRelativeClauses.beq : CorrelativeRelativeClauses → CorrelativeRelativeClauses → Bool

Equations

• Core.WALS.F90E.instBEqCorrelativeRelativeClauses.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.WALS.F90E.instBEqCorrelativeRelativeClauses : BEq CorrelativeRelativeClauses

Equations

• Core.WALS.F90E.instBEqCorrelativeRelativeClauses = { beq := Core.WALS.F90E.instBEqCorrelativeRelativeClauses.beq }

def Core.WALS.F90E.instReprCorrelativeRelativeClauses.repr : CorrelativeRelativeClauses → Nat → Std.Format

Equations

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

instance Core.WALS.F90E.instReprCorrelativeRelativeClauses : Repr CorrelativeRelativeClauses

Equations

• Core.WALS.F90E.instReprCorrelativeRelativeClauses = { reprPrec := Core.WALS.F90E.instReprCorrelativeRelativeClauses.repr }

def Core.WALS.F90E.allData : List (Datapoint CorrelativeRelativeClauses)

Complete WALS 90E dataset (23 languages).

Equations

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

theorem Core.WALS.F90E.total_count : allData.length = 23

theorem Core.WALS.F90E.count_correlativeRelativeClauseDominant : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeRelativeClauseDominant) allData).length = 7

theorem Core.WALS.F90E.count_correlativeOrReln : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeOrReln) allData).length = 7

theorem Core.WALS.F90E.count_correlativeOrNrel : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeOrNrel) allData).length = 2

theorem Core.WALS.F90E.count_correlativeOrInternallyHeaded : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeOrInternallyHeaded) allData).length = 1

theorem Core.WALS.F90E.count_correlativeOrAdjoined : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeOrAdjoined) allData).length = 2

theorem Core.WALS.F90E.count_correlativeAsNondominantType : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeAsNondominantType) allData).length = 3

theorem Core.WALS.F90E.count_correlativeExists : (List.filter (fun (x : Datapoint CorrelativeRelativeClauses) => x.value == CorrelativeRelativeClauses.correlativeExists) allData).length = 1

def Core.WALS.F90E.lookup (code : String) : Option (Datapoint CorrelativeRelativeClauses)

Look up a language by WALS code.

Equations

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

def Core.WALS.F90E.lookupISO (iso : String) : Option (Datapoint CorrelativeRelativeClauses)

Look up a language by ISO 639-3 code.

Equations

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