Documentation

Linglib.Data.WALS.Datapoint

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 Data/WALS/Features/ for the per-feature data files, auto-generated by python3 scripts/gen_wals.py.

source
structure Data.WALS.Datapoint (V : Type) :
Type

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

The human-readable language name is intentionally absent from this struct — each entry already references a walsCode, and Data.WALS.Languages.findLanguage is the canonical lookup for human names. Storing the name in every per-feature entry duplicates ~2660 strings across 192 feature files for no consumer benefit and inflates Lean elaboration time.

  • walsCode : String
  • iso : String
  • value : V
Instances For
    source
    @[implicit_reducible]
    instance Data.WALS.instReprDatapoint {V✝ : Type} [Repr V✝] :
    Repr (Datapoint V✝)
    Equations
    source
    def Data.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.
    Instances For
      source
      @[implicit_reducible]
      instance Data.WALS.instDecidableEqDatapoint {V✝ : Type} [DecidableEq V✝] :
      DecidableEq (Datapoint V✝)
      Equations
      source
      def Data.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.
      Instances For
        source
        def Data.WALS.Datapoint.lookup {V : Type} [BEq V] (data : List (Datapoint V)) (code : String) :
        Option (Datapoint V)

        Look up a language by WALS code.

        Equations
        Instances For
          source
          def Data.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.

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

          Equations
          Instances For