WALS Language Metadata

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

2660 languages referenced across generated features.

structure Data.WALS.Language : Type

WALS language metadata.

• walsCode : String
• name : String
• iso : String
• family : String
• genus : String

@[implicit_reducible]

instance Data.WALS.instReprLanguage : Repr Language

Equations

• Data.WALS.instReprLanguage = { reprPrec := Data.WALS.instReprLanguage.repr }

def Data.WALS.instReprLanguage.repr : Language → Nat → Std.Format

Equations

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

def Data.WALS.instBEqLanguage.beq : Language → Language → Bool

Equations

• One or more equations did not get rendered due to their size.
• Data.WALS.instBEqLanguage.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.WALS.instBEqLanguage : BEq Language

Equations

• Data.WALS.instBEqLanguage = { beq := Data.WALS.instBEqLanguage.beq }

@[implicit_reducible]

instance Data.WALS.instDecidableEqLanguage : DecidableEq Language

Equations

• Data.WALS.instDecidableEqLanguage = Data.WALS.instDecidableEqLanguage.decEq

def Data.WALS.instDecidableEqLanguage.decEq (x✝ x✝¹ : Language) : Decidable (x✝ = x✝¹)

Equations

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

def Data.WALS.languages : List Language

All languages referenced in generated WALS features (2660).

Equations

• Data.WALS.languages = Data.WALS.languages_0✝ ++ Data.WALS.languages_1✝ ++ Data.WALS.languages_2✝ ++ Data.WALS.languages_3✝ ++ Data.WALS.languages_4✝ ++ Data.WALS.languages_5✝

def Data.WALS.findLanguage (code : String) : Option Language

Look up a language by WALS code.

Equations

• Data.WALS.findLanguage code = List.find? (fun (x : Data.WALS.Language) => x.walsCode == code) Data.WALS.languages

def Data.WALS.findByIso (iso : String) : Option Language

Look up a language by ISO 639-3 code.

Returns none for empty queries: WALS marks a handful of languages with an empty iso field, and a naive find? on "" would return one of those entries arbitrarily.

Equations

• Data.WALS.findByIso iso = if iso.isEmpty = true then none else List.find? (fun (x : Data.WALS.Language) => x.iso == iso) Data.WALS.languages