Data.WALS.Aggregation

Shared row struct for WALS distribution tables. Promoted from Linglib/Typology/{Complementation, Morphology, Possession}.lean and Linglib/Phenomena/Polarity/Studies/Haspelmath1997.lean to eliminate the 4-way duplication of this primitive.

WALSCount records a single category label paired with the number of WALS-sampled languages exhibiting that category. WALSCount.totalOf sums the counts over a list of rows (typically the per-chapter distribution).

Substrate-only: depends on no Data/WALS feature files. Each consumer imports this module and constructs its List WALSCount from Data.WALS.F{N}A.allData.

structure Data.WALS.WALSCount : Type

A single row in a WALS frequency table: a category label and the number of WALS-sampled languages with that value.

• label : String
• count : Nat

def Data.WALS.instReprWALSCount.repr : WALSCount → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.WALS.instReprWALSCount : Repr WALSCount

Equations

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

@[implicit_reducible]

instance Data.WALS.instDecidableEqWALSCount : DecidableEq WALSCount

Equations

• Data.WALS.instDecidableEqWALSCount = Data.WALS.instDecidableEqWALSCount.decEq

def Data.WALS.instDecidableEqWALSCount.decEq (x✝ x✝¹ : WALSCount) : Decidable (x✝ = x✝¹)

Equations

• Data.WALS.instDecidableEqWALSCount.decEq { label := a, count := a_1 } { label := b, count := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Data.WALS.WALSCount.totalOf (cs : List WALSCount) : Nat

Sum of count over a list of WALSCount rows.

Equations

• Data.WALS.WALSCount.totalOf cs = List.foldl (fun (acc : Nat) (c : Data.WALS.WALSCount) => acc + c.count) 0 cs