WALS Generic Datapoint

Shared infrastructure for all 192 WALS feature files. Each feature file defines its own inductive type for feature values and a List (Datapoint V) of observations. The generic lookup functions and datapoint structure live here.

See Core/WALS/Features/ for the per-feature data files, auto-generated by python3 scripts/gen_wals.py.

structure Core.WALS.Datapoint (V : Type) : Type

A single WALS datapoint, parameterized by the feature value type V.

• walsCode : String
• language : String
• iso : String
• value : V

def Core.WALS.instReprDatapoint.repr {V✝ : Type} [Repr V✝] : Datapoint V✝ → Nat → Std.Format

Equations

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

instance Core.WALS.instReprDatapoint {V✝ : Type} [Repr V✝] : Repr (Datapoint V✝)

Equations

• Core.WALS.instReprDatapoint = { reprPrec := Core.WALS.instReprDatapoint.repr }

def Core.WALS.instBEqDatapoint.beq {V✝ : Type} [BEq V✝] : Datapoint V✝ → Datapoint V✝ → Bool

Equations

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

instance Core.WALS.instBEqDatapoint {V✝ : Type} [BEq V✝] : BEq (Datapoint V✝)

Equations

• Core.WALS.instBEqDatapoint = { beq := Core.WALS.instBEqDatapoint.beq }

instance Core.WALS.instDecidableEqDatapoint {V✝ : Type} [DecidableEq V✝] : DecidableEq (Datapoint V✝)

Equations

• Core.WALS.instDecidableEqDatapoint = Core.WALS.instDecidableEqDatapoint.decEq

def Core.WALS.instDecidableEqDatapoint.decEq {V✝ : Type} [DecidableEq V✝] (x✝ x✝¹ : Datapoint V✝) : Decidable (x✝ = x✝¹)

Equations

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

def Core.WALS.Datapoint.lookup {V : Type} [BEq V] (data : List (Datapoint V)) (code : String) : Option (Datapoint V)

Look up a language by WALS code.

Equations

• Core.WALS.Datapoint.lookup data code = List.find? (fun (x : Core.WALS.Datapoint V) => x.walsCode == code) data

def Core.WALS.Datapoint.lookupISO {V : Type} [BEq V] (data : List (Datapoint V)) (iso : String) : Option (Datapoint V)

Look up a language by ISO 639-3 code.

Equations

• Core.WALS.Datapoint.lookupISO data iso = List.find? (fun (x : Core.WALS.Datapoint V) => x.iso == iso) data