Typology.ClassifierSystem

@cite{aikhenvald-2000} @cite{chierchia-1998} @cite{dixon-1982} @cite{downing-1996} @cite{allan-1977} @cite{little-moroney-royer-2022} @cite{krifka-1995} @cite{bale-coon-2014} @cite{jenks-2011} @cite{nomoto-2013} @cite{sudo-2016}

Cross-linguistic typology of noun categorization devices, following @cite{aikhenvald-2000} Classifiers: A Typology of Noun Categorization Devices.

Provenance

Merged from Core/Lexical/NounCategorization.lean (vocabulary types: ClassifierType, SemanticParameter, ShapeDimension, CategorizationScope, AssignmentPrinciple, SurfaceRealization, ClassifierEntry, ClassifierStrategy) and the existing Typology/ClassifierSystem.lean (NounCategorizationSystem paradigm record + WALS Ch 55 datapoints) in the cleanup that dissolved Core/Lexical/. Consolidation matches the Typology/PolarityMarking.lean precedent: vocabulary + entry schema

• paradigm record co-located in one file when only one Typology client exists.

Sections

• §1 Aikhenvald classifier types (Table 15.1)
• §2 Semantic parameters (§11.1.1) + shape dimensionality (Downing/Allan)
• §3 Structural properties (assignment, realization, scope)
• §4 ClassifierEntry — per-classifier lexical entry schema
• §5 ClassifierStrategy — competing semantic frameworks (Krifka/B&C/L-M-R vs Chierchia/Jenks/Nomoto/L-M-R vs Sudo blocking)
• §6 NounCategorizationSystem — Aikhenvald 7-property paradigm record
• §7 Prop API for boolean property fields
• §8 Grammatical-category interactions (Table 10.17)
• §9 WALS Ch 55 numeral-classifier status + distribution

What does NOT live here

Theoretical commitments about which strategy mediates the numeral-noun composition (forNoun per Chierchia, sudoBlocking per Sudo) live in the relevant Phenomena/Classifiers/Studies/ files, not on the description here. Cross-paper disagreement is proved as theorems, not embedded as metadata.

Out of scope

@cite{corbett-1991} on gender systems is the obvious adjacent reference for the nounClass constructor; not currently consumed by this file but should be cited if a per-language gender-system substrate gets formalised here. The nounClass cell here collapses what Corbett carefully separates (target gender, controller gender, gender vs. classifier).

inductive Typology.ClassifierType : Type

The 9 focal classifier types on the noun-categorization continuum.

@cite{aikhenvald-2000} establishes these as "focal points" distinguished by morphosyntactic locus, scope, and grammatical function. Real systems are gradient — a language's system may sit between types.

UNVERIFIED: The 9-type taxonomy is Aikhenvald's specific carve-up; other typologists (Allan 1977, Craig 1986, Grinevald 2000, Senft 2000) differ. The nounClass cell here is also more fine-grained per Corbett 1991 — see file docstring "Out of scope".

• nounClass : ClassifierType

  Noun class / gender: closed agreement system, realized outside the noun on modifiers (head-modifier NP) or predicate (pred-arg agreement). Small inventory (2–20). Examples: Bantu, Indo-European gender.

• nounClassifier : ClassifierType

  Noun classifier: independent of other NP elements, characterizes the noun itself. Free forms or affixes on the noun.

• numeralClassifier : ClassifierType

  Numeral classifier: appears in numeral/quantifier NPs, required for enumeration. Free forms or affixes on the numeral.

• relationalClassifier : ClassifierType

  Relational classifier: in possessive NPs, characterizes the possessive relation (how the noun can be possessed/handled).

• possessedClassifier : ClassifierType

  Possessed classifier: in possessive NPs, characterizes the possessed noun in terms of its inherent properties.

• possessorClassifier : ClassifierType

  Possessor classifier: in possessive NPs, characterizes the possessor. Very rare.

• verbalClassifier : ClassifierType

  Verbal classifier: marks agreement on the verb with an S or O argument. Incorporated classifiers, affixes, or suppletive verb stems.

• locativeClassifier : ClassifierType

  Locative classifier: in adpositional NPs, marks agreement with the head noun in locative expressions.

• deicticClassifier : ClassifierType

  Deictic classifier: appears on deictics, articles, demonstratives. Marks spatial location and/or determination.

@[implicit_reducible]

instance Typology.instDecidableEqClassifierType : DecidableEq ClassifierType

Equations

• Typology.instDecidableEqClassifierType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprClassifierType : Repr ClassifierType

Equations

• Typology.instReprClassifierType = { reprPrec := Typology.instReprClassifierType.repr }

def Typology.instReprClassifierType.repr : ClassifierType → Nat → Std.Format

Equations

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

inductive Typology.SemanticParameter : Type

Universal semantic parameters employed in noun categorization.

@cite{aikhenvald-2000} identifies three large classes: animacy, physical properties, and function. These parameters are found across ALL types of noun categorization device, though different types show different preferences.

• animacy : SemanticParameter
• humanness : SemanticParameter
• sex : SemanticParameter
• shape : SemanticParameter
• size : SemanticParameter
• consistency : SemanticParameter
• material : SemanticParameter
• boundedness : SemanticParameter
• function : SemanticParameter
• arrangement : SemanticParameter
• quanta : SemanticParameter
• socialStatus : SemanticParameter
• register : SemanticParameter
• colour : SemanticParameter

@[implicit_reducible]

instance Typology.instDecidableEqSemanticParameter : DecidableEq SemanticParameter

Equations

• Typology.instDecidableEqSemanticParameter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprSemanticParameter : Repr SemanticParameter

Equations

• Typology.instReprSemanticParameter = { reprPrec := Typology.instReprSemanticParameter.repr }

def Typology.instReprSemanticParameter.repr : SemanticParameter → Nat → Std.Format

Equations

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

inductive Typology.ShapeDimension : Type

Dimensionality sub-classification for shape-based classifiers.

@cite{downing-1996} and @cite{allan-1977} show that shape-based classifiers decompose along a dimensionality axis:

• 1D: long, slender, elongated (e.g., Japanese 本 hon, Mandarin 条 tiáo)
• 2D: flat, thin, planar (e.g., Japanese 枚 mai, Mandarin 张 zhāng)
• 3D: round, compact, globular (e.g., Japanese 個 ko)

• oneD : ShapeDimension
• twoD : ShapeDimension
• threeD : ShapeDimension

@[implicit_reducible]

instance Typology.instDecidableEqShapeDimension : DecidableEq ShapeDimension

Equations

• Typology.instDecidableEqShapeDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.instReprShapeDimension.repr : ShapeDimension → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprShapeDimension : Repr ShapeDimension

Equations

• Typology.instReprShapeDimension = { reprPrec := Typology.instReprShapeDimension.repr }

inductive Typology.CategorizationScope : Type

Morphosyntactic scope of a classifier type.

• headModifierNP : CategorizationScope
• predicateArgument : CategorizationScope
• noun : CategorizationScope
• numeralNP : CategorizationScope
• possessiveNP : CategorizationScope
• clause : CategorizationScope
• adpositionalNP : CategorizationScope
• attributiveNP : CategorizationScope

@[implicit_reducible]

instance Typology.instDecidableEqCategorizationScope : DecidableEq CategorizationScope

Equations

• Typology.instDecidableEqCategorizationScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprCategorizationScope : Repr CategorizationScope

Equations

• Typology.instReprCategorizationScope = { reprPrec := Typology.instReprCategorizationScope.repr }

def Typology.instReprCategorizationScope.repr : CategorizationScope → Nat → Std.Format

Equations

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

inductive Typology.AssignmentPrinciple : Type

Principles governing noun-to-class/classifier assignment.

• semantic : AssignmentPrinciple

  Purely semantic: class determined by referent meaning

• morphological : AssignmentPrinciple

  Morphological: class determined by derivational affix, declension, etc.

• phonological : AssignmentPrinciple

  Phonological: class determined by initial segment, final vowel, etc.

• mixed : AssignmentPrinciple

  Mixed: semantic core + morphological/phonological overlay

@[implicit_reducible]

instance Typology.instDecidableEqAssignmentPrinciple : DecidableEq AssignmentPrinciple

Equations

• Typology.instDecidableEqAssignmentPrinciple x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprAssignmentPrinciple : Repr AssignmentPrinciple

Equations

• Typology.instReprAssignmentPrinciple = { reprPrec := Typology.instReprAssignmentPrinciple.repr }

def Typology.instReprAssignmentPrinciple.repr : AssignmentPrinciple → Nat → Std.Format

Equations

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

inductive Typology.SurfaceRealization : Type

Surface realization of a classifier morpheme.

• prefix : SurfaceRealization
• suffix : SurfaceRealization
• clitic : SurfaceRealization
• freeForm : SurfaceRealization
• suppletion : SurfaceRealization
• stress : SurfaceRealization
• reduplication : SurfaceRealization
• nounIncorporation : SurfaceRealization
• repeater : SurfaceRealization

@[implicit_reducible]

instance Typology.instDecidableEqSurfaceRealization : DecidableEq SurfaceRealization

Equations

• Typology.instDecidableEqSurfaceRealization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprSurfaceRealization : Repr SurfaceRealization

Equations

• Typology.instReprSurfaceRealization = { reprPrec := Typology.instReprSurfaceRealization.repr }

def Typology.instReprSurfaceRealization.repr : SurfaceRealization → Nat → Std.Format

Equations

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

structure Typology.ClassifierEntry : Type

A classifier lexical entry with semantic typing.

Each classifier carries its form, a gloss, and the semantic parameters that motivate its selection — making it possible to verify Aikhenvald's claims about which parameters different classifier types encode.

• form : String

  Surface form (e.g. "只", "匹", "本")

• gloss : String

  Gloss (e.g. "small.animal", "flat.bound.object")

• semantics : List SemanticParameter

  Semantic parameters motivating selection of this classifier

• isDefault : Bool

  Is this the "general" or "default" classifier? (个 in Mandarin, つ in Japanese)

• isMensural : Bool

  Sortal (inherent properties) vs. mensural (configuration/measure)

• shapeDimension : Option ShapeDimension

  Shape dimensionality sub-classification (@cite{downing-1996}). Only meaningful when semantics includes .shape.

def Typology.instReprClassifierEntry.repr : ClassifierEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprClassifierEntry : Repr ClassifierEntry

Equations

• Typology.instReprClassifierEntry = { reprPrec := Typology.instReprClassifierEntry.repr }

@[implicit_reducible]

instance Typology.instBEqClassifierEntry : BEq ClassifierEntry

Equations

• Typology.instBEqClassifierEntry = { beq := Typology.instBEqClassifierEntry.beq }

def Typology.instBEqClassifierEntry.beq : ClassifierEntry → ClassifierEntry → Bool

Equations

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

def Typology.ClassifierEntry.encodes (c : ClassifierEntry) (p : SemanticParameter) : Bool

Whether this classifier encodes a given semantic parameter.

Equations

• c.encodes p = c.semantics.any fun (x : Typology.SemanticParameter) => x == p

def Typology.collectSemantics (cls : List ClassifierEntry) : List SemanticParameter

Collect all distinct semantic parameters attested across a classifier inventory. Used to derive preferredSemantics from fragment data rather than hand-listing.

Equations

• Typology.collectSemantics cls = (List.foldl (fun (acc : List Typology.SemanticParameter) (c : Typology.ClassifierEntry) => acc ++ c.semantics) [] cls).eraseDups

inductive Typology.ClassifierStrategy : Type

The semantic strategy a theoretical framework attributes to classifier constructions. Three competing positions are represented:

• forNumeral (CLF-for-NUM): @cite{krifka-1995}, @cite{bale-coon-2014}, @cite{little-moroney-royer-2022}. The classifier is a measure function required by the numeral. The numeral takes the classifier as its first argument: ⟦TWO⟧ = λm⟨e,n⟩λPλx.[P(x) ∧ m(x) = 2]. Predicts: numeral idiosyncrasies in CLF requirement, CLF obligatory even without a noun (counting contexts), CLF + plural marking can co-occur.
• forNoun (CLF-for-N): @cite{chierchia-1998}, @cite{jenks-2011}, @cite{nomoto-2013}, @cite{little-moroney-royer-2022}. The classifier atomizes the noun denotation so the numeral can count. ⟦CLF⟧ = λPλx.[P(x) ∧ ¬∃y[P(y) ∧ y < x]]. Predicts: noun idiosyncrasies in CLF requirement, CLF appears beyond numerals (with quantifiers, demonstratives, relative clauses), CLF + plural marking in complementary distribution.
• sudoBlocking: @cite{sudo-2016}. Classifier semantics live with numerals, not nouns. Numerals are universally type-n singular terms; a phonologically silent ∪-operator type-shifts them to predicates in languages without classifiers, but is blocked (per @cite{chierchia-1998}'s Blocking Principle) in languages whose lexicon contains overt classifiers. Predicts: no numeral or noun idiosyncrasies, CLF appears with numerals not beyond them, CLF appears in counting contexts (via the ∩-operator).

Strategy assignments to specific languages live in study files (Phenomena/Classifiers/Studies/{NMP,LittleMoroneyRoyer2022,Sudo2016}.lean), not in this file or in NounCategorizationSystem. Each paper owns its own per-language commitments; cross-paper agreement and disagreement are first-class theorems in the study files.

• forNumeral : ClassifierStrategy
• forNoun : ClassifierStrategy
• sudoBlocking : ClassifierStrategy

@[implicit_reducible]

instance Typology.instDecidableEqClassifierStrategy : DecidableEq ClassifierStrategy

Equations

• Typology.instDecidableEqClassifierStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprClassifierStrategy : Repr ClassifierStrategy

Equations

• Typology.instReprClassifierStrategy = { reprPrec := Typology.instReprClassifierStrategy.repr }

def Typology.instReprClassifierStrategy.repr : ClassifierStrategy → Nat → Std.Format

Equations

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

structure Typology.NounCategorizationSystem : Type

A noun categorization system in a language.

Captures @cite{aikhenvald-2000}'s 7 definitional properties (A–G): (A) morphosyntactic locus → scopes (B) scope/domain → classifierType + scopes (C) assignment principles → assignment (D) surface realization → realizations (E) agreement → hasAgreement (F) markedness → hasUnmarkedDefault (G) grammaticalization → isObligatory

UNVERIFIED: A–G enumeration cited from memory.

• family : String

  Language family (e.g., "Indo-European", "Sino-Tibetan", "Bantu").

• classifierType : ClassifierType

  Aikhenvald classifier type.

• scopes : List CategorizationScope

  Morphosyntactic scopes this system operates in (A, B).

• assignment : AssignmentPrinciple

  How nouns are assigned to classes/classifiers (C).

• realizations : List SurfaceRealization

  Morphological realization types used (D).

• hasAgreement : Bool

  Does the system involve agreement? (E) — definitional for noun classes. Stored as Bool so the struct stays decidable as a whole; the user-facing predicate is HasAgreement : Prop.

• inventorySize : Nat

  Inventory size (number of classes or classifiers).

• isObligatory : Bool

  Is realization obligatory or optional? (G). User-facing predicate: IsObligatory : Prop.

• hasUnmarkedDefault : Bool

  Is there a formally/functionally unmarked default? (F). User-facing predicate: HasUnmarkedDefault : Prop.

• preferredSemantics : List SemanticParameter

  Preferred semantic parameters (Aikhenvald §11.2).

• hasObligatoryNumber : Bool

  Does the language have obligatory grammatical number marking? User-facing predicate: HasObligatoryNumber : Prop.

• pluralClfCooccur : Bool

  Can classifiers and plural marking co-occur? Predicted by CLF-for-NUM (@cite{little-moroney-royer-2022}: CLF and PL are in different projections) but not by CLF-for-N (same projection, complementary distribution per @cite{borer-2005}). User-facing predicate: PluralClfCooccur : Prop.

• source : String

  Citation backing the hand-coded values.

def Typology.instReprNounCategorizationSystem.repr : NounCategorizationSystem → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprNounCategorizationSystem : Repr NounCategorizationSystem

Equations

• Typology.instReprNounCategorizationSystem = { reprPrec := Typology.instReprNounCategorizationSystem.repr }

@[implicit_reducible]

instance Typology.instDecidableEqNounCategorizationSystem : DecidableEq NounCategorizationSystem

Equations

• Typology.instDecidableEqNounCategorizationSystem = Typology.instDecidableEqNounCategorizationSystem.decEq

def Typology.instDecidableEqNounCategorizationSystem.decEq (x✝ x✝¹ : NounCategorizationSystem) : Decidable (x✝ = x✝¹)

Equations

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

Prop API for the boolean property fields

The struct's hasAgreement/isObligatory/hasUnmarkedDefault/ hasObligatoryNumber/pluralClfCooccur fields are stored as Bool so the struct itself stays decidably equal. The user-facing predicates are the Prop versions defined here, each with a Decidable instance via the underlying Bool. Theorem statements should prefer the Prop form (s.HasAgreement rather than s.hasAgreement = true); decide works for either since the Bool projection reduces structurally for concrete fragment values.

@[reducible, inline]

abbrev Typology.NounCategorizationSystem.HasAgreement (s : NounCategorizationSystem) : Prop

The system involves agreement (E).

Equations

• s.HasAgreement = (s.hasAgreement = true)

@[reducible, inline]

abbrev Typology.NounCategorizationSystem.IsObligatory (s : NounCategorizationSystem) : Prop

Realization is obligatory (G).

Equations

• s.IsObligatory = (s.isObligatory = true)

@[reducible, inline]

abbrev Typology.NounCategorizationSystem.HasUnmarkedDefault (s : NounCategorizationSystem) : Prop

The system has a formally/functionally unmarked default (F).

Equations

• s.HasUnmarkedDefault = (s.hasUnmarkedDefault = true)

@[reducible, inline]

abbrev Typology.NounCategorizationSystem.HasObligatoryNumber (s : NounCategorizationSystem) : Prop

The language has obligatory grammatical number marking.

Equations

• s.HasObligatoryNumber = (s.hasObligatoryNumber = true)

@[reducible, inline]

abbrev Typology.NounCategorizationSystem.PluralClfCooccur (s : NounCategorizationSystem) : Prop

Classifiers and plural marking can co-occur.

Equations

• s.PluralClfCooccur = (s.pluralClfCooccur = true)

def Typology.NounCategorizationSystem.isNounClassType (t : ClassifierType) : Bool

@cite{dixon-1982}'s noun-class vs. classifier divide. Noun classes: small, closed, grammaticalized, agreement. Classifiers: large, open, lexical, no agreement.

Equations

• Typology.NounCategorizationSystem.isNounClassType t = (t == Typology.ClassifierType.nounClass)

def Typology.NounCategorizationSystem.isClassifierType (t : ClassifierType) : Bool

All non-noun-class types are "classifier" types in the broad sense.

Equations

• Typology.NounCategorizationSystem.isClassifierType t = !Typology.NounCategorizationSystem.isNounClassType t

inductive Typology.GrammaticalCategory : Type

Grammatical categories that interact with classifier types (@cite{aikhenvald-2000}).

• definiteness : GrammaticalCategory
• number : GrammaticalCategory
• case_ : GrammaticalCategory
• tenseAspect : GrammaticalCategory
• possession : GrammaticalCategory

@[implicit_reducible]

instance Typology.instDecidableEqGrammaticalCategory : DecidableEq GrammaticalCategory

Equations

• Typology.instDecidableEqGrammaticalCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprGrammaticalCategory : Repr GrammaticalCategory

Equations

• Typology.instReprGrammaticalCategory = { reprPrec := Typology.instReprGrammaticalCategory.repr }

def Typology.instReprGrammaticalCategory.repr : GrammaticalCategory → Nat → Std.Format

Equations

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

def Typology.interacts : ClassifierType → GrammaticalCategory → Bool

Whether a classifier type typically interacts with a grammatical category (@cite{aikhenvald-2000}).

Equations

• Typology.interacts Typology.ClassifierType.nounClass Typology.GrammaticalCategory.definiteness = true
• Typology.interacts Typology.ClassifierType.nounClass Typology.GrammaticalCategory.number = true
• Typology.interacts Typology.ClassifierType.nounClass Typology.GrammaticalCategory.case_ = true
• Typology.interacts Typology.ClassifierType.nounClass Typology.GrammaticalCategory.tenseAspect = true
• Typology.interacts Typology.ClassifierType.nounClass Typology.GrammaticalCategory.possession = true
• Typology.interacts Typology.ClassifierType.numeralClassifier Typology.GrammaticalCategory.definiteness = true
• Typology.interacts Typology.ClassifierType.numeralClassifier Typology.GrammaticalCategory.number = true
• Typology.interacts Typology.ClassifierType.numeralClassifier Typology.GrammaticalCategory.possession = false
• Typology.interacts Typology.ClassifierType.numeralClassifier Typology.GrammaticalCategory.case_ = false
• Typology.interacts Typology.ClassifierType.numeralClassifier Typology.GrammaticalCategory.tenseAspect = false
• Typology.interacts Typology.ClassifierType.verbalClassifier Typology.GrammaticalCategory.tenseAspect = true
• Typology.interacts Typology.ClassifierType.verbalClassifier Typology.GrammaticalCategory.number = true
• Typology.interacts Typology.ClassifierType.relationalClassifier Typology.GrammaticalCategory.possession = true
• Typology.interacts Typology.ClassifierType.possessedClassifier Typology.GrammaticalCategory.possession = true
• Typology.interacts x✝¹ x✝ = false

inductive Typology.ClassifierStatus : Type

Whether a language uses numeral classifiers (@cite{wals-2013} Ch 55).

• absent : ClassifierStatus

  No numeral classifiers (e.g., English, Spanish, Arabic).

• optional : ClassifierStatus

  Classifiers available but not required (e.g., Turkish, Bengali).

• obligatory : ClassifierStatus

  Classifiers required (e.g., Mandarin, Japanese, Thai).

@[implicit_reducible]

instance Typology.instDecidableEqClassifierStatus : DecidableEq ClassifierStatus

Equations

• Typology.instDecidableEqClassifierStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.instReprClassifierStatus : Repr ClassifierStatus

Equations

• Typology.instReprClassifierStatus = { reprPrec := Typology.instReprClassifierStatus.repr }

def Typology.instReprClassifierStatus.repr : ClassifierStatus → Nat → Std.Format

Equations

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

def Typology.fromWALS55A : Data.WALS.F55A.NumeralClassifiers → ClassifierStatus

Convert WALS 55A numeral classifier values to the local ClassifierStatus.

Equations

• Typology.fromWALS55A Data.WALS.F55A.NumeralClassifiers.absent = Typology.ClassifierStatus.absent
• Typology.fromWALS55A Data.WALS.F55A.NumeralClassifiers.optional = Typology.ClassifierStatus.optional
• Typology.fromWALS55A Data.WALS.F55A.NumeralClassifiers.obligatory = Typology.ClassifierStatus.obligatory

structure Typology.ClassifierDistribution : Type

WALS Chapter 55 distribution: language counts per classifier status. Total: 400 languages.

• absent : Nat
• optional : Nat
• obligatory : Nat

@[implicit_reducible]

instance Typology.instReprClassifierDistribution : Repr ClassifierDistribution

Equations

• Typology.instReprClassifierDistribution = { reprPrec := Typology.instReprClassifierDistribution.repr }

def Typology.instReprClassifierDistribution.repr : ClassifierDistribution → Nat → Std.Format

Equations

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

def Typology.ClassifierDistribution.total (d : ClassifierDistribution) : Nat

Equations

• d.total = d.absent + d.optional + d.obligatory

def Typology.ch55Distribution : ClassifierDistribution

Actual WALS Ch 55 counts (260 absent + 62 optional + 78 obligatory = 400).

Equations

• Typology.ch55Distribution = { absent := 260, optional := 62, obligatory := 78 }