Lexical Typology (WALS Chapters 129--142)

@cite{dryer-haspelmath-2013}

Cross-linguistic data on lexical categorization from 16 WALS features spanning body-part terminology (Ch 129--130), colour terminology (Ch 132--135), pronominal root patterns (Ch 136--137), the Wanderwort "tea" (Ch 138), sign language features (Ch 139--140), writing systems (Ch 141), and para-linguistic click usage (Ch 142).

These chapters address a question that sits at the intersection of lexical semantics and anthropological linguistics: how do languages carve up conceptual space into words? The body-part and colour chapters are classic case studies in the universals-vs-relativity debate. The pronoun chapters probe whether certain phonological shapes are universally associated with person reference. The tea chapter traces a single Wanderwort across the globe, providing a window into contact history through lexical borrowing.

Body-Part Terms (Ch 129--130)

• F129A: Hand and Arm -- whether a language uses the same or different words for 'hand' and 'arm'. Identical forms (228/617 = 37%) vs distinct forms (389/617 = 63%).
• F130A: Finger and Hand -- whether a language uses the same or different words for 'finger' and 'hand'. Identical forms are rare (72/593 = 12%).
• F130B: Cultural Categories -- among languages with finger=hand identity, the cultural type: hunter-gatherers (46/72), farmer-foragers (18/72), full-fledged farmers (8/72).

Colour Terms (Ch 132--135)

• F132A: Non-Derived Basic Colour Categories -- how many non-derived basic colour categories a language has (3 to 6).
• F133A: Basic Colour Categories -- total number of basic colour categories including derived ones (3--4 to 11).
• F134A: Green and Blue -- whether a language distinguishes green from blue, merges them (grue), or has other patterns.
• F135A: Red and Yellow -- whether a language distinguishes red from yellow or merges them.

Pronominal Roots (Ch 136--137)

• F136A: M-T Pronouns -- whether the language has an m/t pattern in 1SG/2SG pronouns (paradigmatic or non-paradigmatic).
• F136B: M in 1SG -- whether 1SG has an m-initial form.
• F137A: N-M Pronouns -- whether the language has an n/m pattern in 1SG/2SG pronouns.
• F137B: M in 2SG -- whether 2SG has an m-initial form.

Tea (Ch 138)

• F138A: Tea -- whether the word for 'tea' derives from Sinitic cha, Min Nan te, or is an independent form.

Sign Language Features (Ch 139--140)

• F139A: Irregular Negatives -- how many irregular negative signs a sign language has.
• F140A: Question Particles -- whether a sign language uses question particles.

Writing Systems (Ch 141) and Clicks (Ch 142)

• F141A: Writing Systems -- type of writing system (only 6 languages in WALS sample; highly incomplete).
• F142A: Para-Linguistic Usages of Clicks -- whether clicks are used for logical meanings (negation/affirmation) or affective meanings (disgust/annoyance).

inductive Phenomena.LexicalTypology.Typology.HandArmRelation : Type

Whether a language uses the same or different lexemes for 'hand' and 'arm'. Many languages worldwide use a single term covering both concepts (e.g., Japanese te, Russian ruka), while others lexically distinguish them (e.g., English hand vs arm).

• identical : HandArmRelation

  The same word covers both 'hand' and 'arm'.

• different : HandArmRelation

  Distinct words for 'hand' and 'arm'.

instance Phenomena.LexicalTypology.Typology.instDecidableEqHandArmRelation : DecidableEq HandArmRelation

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqHandArmRelation.beq : HandArmRelation → HandArmRelation → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqHandArmRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqHandArmRelation : BEq HandArmRelation

Equations

• Phenomena.LexicalTypology.Typology.instBEqHandArmRelation = { beq := Phenomena.LexicalTypology.Typology.instBEqHandArmRelation.beq }

def Phenomena.LexicalTypology.Typology.instReprHandArmRelation.repr : HandArmRelation → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprHandArmRelation : Repr HandArmRelation

Equations

• Phenomena.LexicalTypology.Typology.instReprHandArmRelation = { reprPrec := Phenomena.LexicalTypology.Typology.instReprHandArmRelation.repr }

inductive Phenomena.LexicalTypology.Typology.FingerHandRelation : Type

Whether a language uses the same or different lexemes for 'finger' and 'hand'. Identity of 'finger' and 'hand' is cross-linguistically rare (12% of sample) and correlates with subsistence type.

• identical : FingerHandRelation

  The same word covers both 'finger' and 'hand'.

• different : FingerHandRelation

  Distinct words for 'finger' and 'hand'.

instance Phenomena.LexicalTypology.Typology.instDecidableEqFingerHandRelation : DecidableEq FingerHandRelation

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqFingerHandRelation.beq : FingerHandRelation → FingerHandRelation → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqFingerHandRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqFingerHandRelation : BEq FingerHandRelation

Equations

• Phenomena.LexicalTypology.Typology.instBEqFingerHandRelation = { beq := Phenomena.LexicalTypology.Typology.instBEqFingerHandRelation.beq }

def Phenomena.LexicalTypology.Typology.instReprFingerHandRelation.repr : FingerHandRelation → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprFingerHandRelation : Repr FingerHandRelation

Equations

• Phenomena.LexicalTypology.Typology.instReprFingerHandRelation = { reprPrec := Phenomena.LexicalTypology.Typology.instReprFingerHandRelation.repr }

inductive Phenomena.LexicalTypology.Typology.NonDerivedColourCount : Type

Number of non-derived basic colour categories (F132A). Follows the Berlin & Kay hierarchy: languages range from 3 to 6 non-derived basic colour terms.

• three : NonDerivedColourCount
• threeHalf : NonDerivedColourCount
• four : NonDerivedColourCount
• fourHalf : NonDerivedColourCount
• five : NonDerivedColourCount
• fiveHalf : NonDerivedColourCount
• six : NonDerivedColourCount

instance Phenomena.LexicalTypology.Typology.instDecidableEqNonDerivedColourCount : DecidableEq NonDerivedColourCount

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqNonDerivedColourCount.beq : NonDerivedColourCount → NonDerivedColourCount → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqNonDerivedColourCount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqNonDerivedColourCount : BEq NonDerivedColourCount

Equations

• Phenomena.LexicalTypology.Typology.instBEqNonDerivedColourCount = { beq := Phenomena.LexicalTypology.Typology.instBEqNonDerivedColourCount.beq }

def Phenomena.LexicalTypology.Typology.instReprNonDerivedColourCount.repr : NonDerivedColourCount → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprNonDerivedColourCount : Repr NonDerivedColourCount

Equations

• Phenomena.LexicalTypology.Typology.instReprNonDerivedColourCount = { reprPrec := Phenomena.LexicalTypology.Typology.instReprNonDerivedColourCount.repr }

inductive Phenomena.LexicalTypology.Typology.BasicColourCount : Type

Total number of basic colour categories including derived ones (F133A). Ranges from 3--4 (minimal systems) to 11 (maximal, e.g., English, Russian).

• v3to4 : BasicColourCount
• v4to5 : BasicColourCount
• v6to6h : BasicColourCount
• v7to7h : BasicColourCount
• v8to8h : BasicColourCount
• v9to10 : BasicColourCount
• v11 : BasicColourCount

instance Phenomena.LexicalTypology.Typology.instDecidableEqBasicColourCount : DecidableEq BasicColourCount

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqBasicColourCount : BEq BasicColourCount

Equations

• Phenomena.LexicalTypology.Typology.instBEqBasicColourCount = { beq := Phenomena.LexicalTypology.Typology.instBEqBasicColourCount.beq }

def Phenomena.LexicalTypology.Typology.instBEqBasicColourCount.beq : BasicColourCount → BasicColourCount → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqBasicColourCount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instReprBasicColourCount : Repr BasicColourCount

Equations

• Phenomena.LexicalTypology.Typology.instReprBasicColourCount = { reprPrec := Phenomena.LexicalTypology.Typology.instReprBasicColourCount.repr }

def Phenomena.LexicalTypology.Typology.instReprBasicColourCount.repr : BasicColourCount → Nat → Std.Format

Equations

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

inductive Phenomena.LexicalTypology.Typology.GreenBlueRelation : Type

How a language treats the green-blue region of colour space (F134A). The classic grue/green-blue distinction.

• distinct : GreenBlueRelation

  Separate terms for green and blue.

• merged : GreenBlueRelation

  A single 'grue' term covering both green and blue.

• blackGreenBlue : GreenBlueRelation

  A single term covering black, green, and blue.

• blackBlueVsGreen : GreenBlueRelation

  Black/blue merged, green separate.

• yellowGreenBlue : GreenBlueRelation

  Yellow, green, blue all merged.

• yellowGreenVsBlue : GreenBlueRelation

  Yellow/green merged, blue separate.

• noTerm : GreenBlueRelation

  No green or blue term at all.

instance Phenomena.LexicalTypology.Typology.instDecidableEqGreenBlueRelation : DecidableEq GreenBlueRelation

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqGreenBlueRelation : BEq GreenBlueRelation

Equations

• Phenomena.LexicalTypology.Typology.instBEqGreenBlueRelation = { beq := Phenomena.LexicalTypology.Typology.instBEqGreenBlueRelation.beq }

def Phenomena.LexicalTypology.Typology.instBEqGreenBlueRelation.beq : GreenBlueRelation → GreenBlueRelation → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqGreenBlueRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instReprGreenBlueRelation : Repr GreenBlueRelation

Equations

• Phenomena.LexicalTypology.Typology.instReprGreenBlueRelation = { reprPrec := Phenomena.LexicalTypology.Typology.instReprGreenBlueRelation.repr }

def Phenomena.LexicalTypology.Typology.instReprGreenBlueRelation.repr : GreenBlueRelation → Nat → Std.Format

Equations

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

inductive Phenomena.LexicalTypology.Typology.RedYellowRelation : Type

How a language treats the red-yellow region of colour space (F135A).

• distinct : RedYellowRelation

  Separate terms for red and yellow.

• merged : RedYellowRelation

  A single term covering both red and yellow.

• yellowGreenBlueVsRed : RedYellowRelation

  Yellow/green/blue merged, vs red.

• yellowGreenVsRed : RedYellowRelation

  Yellow/green merged, vs red.

• noTerm : RedYellowRelation

  No red or yellow term at all.

instance Phenomena.LexicalTypology.Typology.instDecidableEqRedYellowRelation : DecidableEq RedYellowRelation

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqRedYellowRelation : BEq RedYellowRelation

Equations

• Phenomena.LexicalTypology.Typology.instBEqRedYellowRelation = { beq := Phenomena.LexicalTypology.Typology.instBEqRedYellowRelation.beq }

def Phenomena.LexicalTypology.Typology.instBEqRedYellowRelation.beq : RedYellowRelation → RedYellowRelation → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqRedYellowRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instReprRedYellowRelation : Repr RedYellowRelation

Equations

• Phenomena.LexicalTypology.Typology.instReprRedYellowRelation = { reprPrec := Phenomena.LexicalTypology.Typology.instReprRedYellowRelation.repr }

def Phenomena.LexicalTypology.Typology.instReprRedYellowRelation.repr : RedYellowRelation → Nat → Std.Format

Equations

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

inductive Phenomena.LexicalTypology.Typology.MTPronounPattern : Type

M-T pronoun pattern (F136A): whether 1SG has /m/ and 2SG has /t/, a widespread cross-linguistic pattern noted by many typologists.

• absent : MTPronounPattern

  No M-T pattern in the pronoun paradigm.

• paradigmatic : MTPronounPattern

  M-T pattern is paradigmatic (systematic across forms).

• nonParadigmatic : MTPronounPattern

  M-T pattern is non-paradigmatic (sporadic).

instance Phenomena.LexicalTypology.Typology.instDecidableEqMTPronounPattern : DecidableEq MTPronounPattern

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqMTPronounPattern : BEq MTPronounPattern

Equations

• Phenomena.LexicalTypology.Typology.instBEqMTPronounPattern = { beq := Phenomena.LexicalTypology.Typology.instBEqMTPronounPattern.beq }

def Phenomena.LexicalTypology.Typology.instBEqMTPronounPattern.beq : MTPronounPattern → MTPronounPattern → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqMTPronounPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.LexicalTypology.Typology.instReprMTPronounPattern.repr : MTPronounPattern → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprMTPronounPattern : Repr MTPronounPattern

Equations

• Phenomena.LexicalTypology.Typology.instReprMTPronounPattern = { reprPrec := Phenomena.LexicalTypology.Typology.instReprMTPronounPattern.repr }

inductive Phenomena.LexicalTypology.Typology.MIn1SG : Type

Whether 1SG has an m-initial or m-containing form (F136B).

• absent : MIn1SG
• present : MIn1SG

instance Phenomena.LexicalTypology.Typology.instDecidableEqMIn1SG : DecidableEq MIn1SG

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqMIn1SG.beq : MIn1SG → MIn1SG → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqMIn1SG.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqMIn1SG : BEq MIn1SG

Equations

• Phenomena.LexicalTypology.Typology.instBEqMIn1SG = { beq := Phenomena.LexicalTypology.Typology.instBEqMIn1SG.beq }

def Phenomena.LexicalTypology.Typology.instReprMIn1SG.repr : MIn1SG → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprMIn1SG : Repr MIn1SG

Equations

• Phenomena.LexicalTypology.Typology.instReprMIn1SG = { reprPrec := Phenomena.LexicalTypology.Typology.instReprMIn1SG.repr }

inductive Phenomena.LexicalTypology.Typology.NMPronounPattern : Type

N-M pronoun pattern (F137A): whether 1SG has /n/ and 2SG has /m/.

• absent : NMPronounPattern

  No N-M pattern.

• paradigmatic : NMPronounPattern

  N-M pattern is paradigmatic.

• nonParadigmatic : NMPronounPattern

  N-M pattern is non-paradigmatic.

instance Phenomena.LexicalTypology.Typology.instDecidableEqNMPronounPattern : DecidableEq NMPronounPattern

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqNMPronounPattern.beq : NMPronounPattern → NMPronounPattern → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqNMPronounPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqNMPronounPattern : BEq NMPronounPattern

Equations

• Phenomena.LexicalTypology.Typology.instBEqNMPronounPattern = { beq := Phenomena.LexicalTypology.Typology.instBEqNMPronounPattern.beq }

def Phenomena.LexicalTypology.Typology.instReprNMPronounPattern.repr : NMPronounPattern → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprNMPronounPattern : Repr NMPronounPattern

Equations

• Phenomena.LexicalTypology.Typology.instReprNMPronounPattern = { reprPrec := Phenomena.LexicalTypology.Typology.instReprNMPronounPattern.repr }

inductive Phenomena.LexicalTypology.Typology.MIn2SG : Type

Whether 2SG has an m-initial or m-containing form (F137B).

• absent : MIn2SG
• present : MIn2SG

instance Phenomena.LexicalTypology.Typology.instDecidableEqMIn2SG : DecidableEq MIn2SG

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqMIn2SG : BEq MIn2SG

Equations

• Phenomena.LexicalTypology.Typology.instBEqMIn2SG = { beq := Phenomena.LexicalTypology.Typology.instBEqMIn2SG.beq }

def Phenomena.LexicalTypology.Typology.instBEqMIn2SG.beq : MIn2SG → MIn2SG → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqMIn2SG.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instReprMIn2SG : Repr MIn2SG

Equations

• Phenomena.LexicalTypology.Typology.instReprMIn2SG = { reprPrec := Phenomena.LexicalTypology.Typology.instReprMIn2SG.repr }

def Phenomena.LexicalTypology.Typology.instReprMIn2SG.repr : MIn2SG → Nat → Std.Format

Equations

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

inductive Phenomena.LexicalTypology.Typology.TeaWordOrigin : Type

Origin of the word for 'tea' (F138A). One of the most striking Wanderworter: nearly all words for tea worldwide derive from either Sinitic cha (spread overland via the Silk Road) or Min Nan te (spread by sea via Dutch trade).

• cha : TeaWordOrigin

  Derived from Sinitic cha (e.g., Hindi chai, Russian chaj, Turkish cay, Japanese cha, Arabic shay).

• te : TeaWordOrigin

  Derived from Min Nan Chinese te (e.g., English tea, French the, German Tee, Spanish te, Finnish tee).

• other : TeaWordOrigin

  Independent form, not from either source.

instance Phenomena.LexicalTypology.Typology.instDecidableEqTeaWordOrigin : DecidableEq TeaWordOrigin

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqTeaWordOrigin : BEq TeaWordOrigin

Equations

• Phenomena.LexicalTypology.Typology.instBEqTeaWordOrigin = { beq := Phenomena.LexicalTypology.Typology.instBEqTeaWordOrigin.beq }

def Phenomena.LexicalTypology.Typology.instBEqTeaWordOrigin.beq : TeaWordOrigin → TeaWordOrigin → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqTeaWordOrigin.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instReprTeaWordOrigin : Repr TeaWordOrigin

Equations

• Phenomena.LexicalTypology.Typology.instReprTeaWordOrigin = { reprPrec := Phenomena.LexicalTypology.Typology.instReprTeaWordOrigin.repr }

def Phenomena.LexicalTypology.Typology.instReprTeaWordOrigin.repr : TeaWordOrigin → Nat → Std.Format

Equations

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

inductive Phenomena.LexicalTypology.Typology.IrregularNegativeCount : Type

Number of irregular negative signs in a sign language (F139A).

• none : IrregularNegativeCount
• one : IrregularNegativeCount
• some : IrregularNegativeCount
• many : IrregularNegativeCount

instance Phenomena.LexicalTypology.Typology.instDecidableEqIrregularNegativeCount : DecidableEq IrregularNegativeCount

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqIrregularNegativeCount.beq : IrregularNegativeCount → IrregularNegativeCount → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqIrregularNegativeCount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqIrregularNegativeCount : BEq IrregularNegativeCount

Equations

• Phenomena.LexicalTypology.Typology.instBEqIrregularNegativeCount = { beq := Phenomena.LexicalTypology.Typology.instBEqIrregularNegativeCount.beq }

instance Phenomena.LexicalTypology.Typology.instReprIrregularNegativeCount : Repr IrregularNegativeCount

Equations

• Phenomena.LexicalTypology.Typology.instReprIrregularNegativeCount = { reprPrec := Phenomena.LexicalTypology.Typology.instReprIrregularNegativeCount.repr }

def Phenomena.LexicalTypology.Typology.instReprIrregularNegativeCount.repr : IrregularNegativeCount → Nat → Std.Format

Equations

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

inductive Phenomena.LexicalTypology.Typology.SignQuestionParticle : Type

Question particle usage in sign languages (F140A).

• none : SignQuestionParticle
• one : SignQuestionParticle
• moreThanOne : SignQuestionParticle

instance Phenomena.LexicalTypology.Typology.instDecidableEqSignQuestionParticle : DecidableEq SignQuestionParticle

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqSignQuestionParticle.beq : SignQuestionParticle → SignQuestionParticle → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqSignQuestionParticle.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqSignQuestionParticle : BEq SignQuestionParticle

Equations

• Phenomena.LexicalTypology.Typology.instBEqSignQuestionParticle = { beq := Phenomena.LexicalTypology.Typology.instBEqSignQuestionParticle.beq }

def Phenomena.LexicalTypology.Typology.instReprSignQuestionParticle.repr : SignQuestionParticle → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprSignQuestionParticle : Repr SignQuestionParticle

Equations

• Phenomena.LexicalTypology.Typology.instReprSignQuestionParticle = { reprPrec := Phenomena.LexicalTypology.Typology.instReprSignQuestionParticle.repr }

inductive Phenomena.LexicalTypology.Typology.WritingSystemType : Type

Type of writing system (F141A). Note: WALS sample is tiny (6 languages) and only covers non-alphabetic systems in the Americas and West Africa.

• alphabetic : WritingSystemType
• consonantal : WritingSystemType
• alphasyllabic : WritingSystemType
• syllabic : WritingSystemType
• logographic : WritingSystemType
• mixedLogographicSyllabic : WritingSystemType

instance Phenomena.LexicalTypology.Typology.instDecidableEqWritingSystemType : DecidableEq WritingSystemType

Equations

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

def Phenomena.LexicalTypology.Typology.instBEqWritingSystemType.beq : WritingSystemType → WritingSystemType → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqWritingSystemType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.LexicalTypology.Typology.instBEqWritingSystemType : BEq WritingSystemType

Equations

• Phenomena.LexicalTypology.Typology.instBEqWritingSystemType = { beq := Phenomena.LexicalTypology.Typology.instBEqWritingSystemType.beq }

def Phenomena.LexicalTypology.Typology.instReprWritingSystemType.repr : WritingSystemType → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprWritingSystemType : Repr WritingSystemType

Equations

• Phenomena.LexicalTypology.Typology.instReprWritingSystemType = { reprPrec := Phenomena.LexicalTypology.Typology.instReprWritingSystemType.repr }

inductive Phenomena.LexicalTypology.Typology.ClickUsage : Type

Para-linguistic usage of clicks (F142A). Click sounds are used para-linguistically even in languages that lack phonemic clicks.

• logical : ClickUsage

  Clicks used for logical meanings: negation ("tsk-tsk" = no), affirmation, or other propositional functions.

• affective : ClickUsage

  Clicks used for affective/expressive meanings: annoyance, disapproval, sympathy, or attention-getting.

• otherOrNone : ClickUsage

  Other usage or no para-linguistic clicks attested.

instance Phenomena.LexicalTypology.Typology.instDecidableEqClickUsage : DecidableEq ClickUsage

Equations

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

instance Phenomena.LexicalTypology.Typology.instBEqClickUsage : BEq ClickUsage

Equations

• Phenomena.LexicalTypology.Typology.instBEqClickUsage = { beq := Phenomena.LexicalTypology.Typology.instBEqClickUsage.beq }

def Phenomena.LexicalTypology.Typology.instBEqClickUsage.beq : ClickUsage → ClickUsage → Bool

Equations

• Phenomena.LexicalTypology.Typology.instBEqClickUsage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.LexicalTypology.Typology.instReprClickUsage.repr : ClickUsage → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprClickUsage : Repr ClickUsage

Equations

• Phenomena.LexicalTypology.Typology.instReprClickUsage = { reprPrec := Phenomena.LexicalTypology.Typology.instReprClickUsage.repr }

structure Phenomena.LexicalTypology.Typology.LexicalProfile : Type

A language's lexical typology profile across WALS Chapters 129--142. Fields are Option because coverage varies enormously across features: the body-part chapters cover ~600 languages, the pronoun/tea chapters cover ~230, the colour chapters ~120, and writing systems only 6.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• family : String

  Language family.

• handArm : Option HandArmRelation

  F129A: Whether 'hand' and 'arm' are the same word.

• fingerHand : Option FingerHandRelation

  F130A: Whether 'finger' and 'hand' are the same word.

• nonDerivedColours : Option NonDerivedColourCount

  F132A: Number of non-derived basic colour categories.

• basicColours : Option BasicColourCount

  F133A: Total number of basic colour categories.

• greenBlue : Option GreenBlueRelation

  F134A: Green-blue distinction.

• redYellow : Option RedYellowRelation

  F135A: Red-yellow distinction.

• mtPronouns : Option MTPronounPattern

  F136A: M-T pronoun pattern.

• mIn1sg : Option MIn1SG

  F136B: M in 1SG.

• nmPronouns : Option NMPronounPattern

  F137A: N-M pronoun pattern.

• mIn2sg : Option MIn2SG

  F137B: M in 2SG.

• tea : Option TeaWordOrigin

  F138A: Origin of the word for 'tea'.

• clicks : Option ClickUsage

  F142A: Para-linguistic click usage.

def Phenomena.LexicalTypology.Typology.instReprLexicalProfile.repr : LexicalProfile → Nat → Std.Format

Equations

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

instance Phenomena.LexicalTypology.Typology.instReprLexicalProfile : Repr LexicalProfile

Equations

• Phenomena.LexicalTypology.Typology.instReprLexicalProfile = { reprPrec := Phenomena.LexicalTypology.Typology.instReprLexicalProfile.repr }

def Phenomena.LexicalTypology.Typology.english : LexicalProfile

English (Indo-European, Germanic). Distinct hand/arm and finger/hand. 6 non-derived colour categories, 11 total basic colours (the Berlin-Kay maximum). Green and blue are distinct; red and yellow are distinct. No M-T pronoun pattern but 1SG "me/my" has /m/. Tea from Min Nan te. Clicks used affectively (tut-tut for disapproval).

Equations

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

def Phenomena.LexicalTypology.Typology.french : LexicalProfile

French (Indo-European, Romance). Distinct hand/arm (main vs bras) and finger/hand (doigt vs main). 6 non-derived, 11 total colour categories. Green (vert) and blue (bleu) distinct. M-T paradigmatic (moi/toi). Tea from te (the).

Equations

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

def Phenomena.LexicalTypology.Typology.german : LexicalProfile

German (Indo-European, Germanic). Distinct hand/arm (Hand vs Arm) and finger/hand (Finger vs Hand). 6 non-derived, 11 total colour categories. Green (grun) and blue (blau) distinct. M-T paradigmatic (mich/dich). Tea from te (Tee). Clicks used affectively.

Equations

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

def Phenomena.LexicalTypology.Typology.spanish : LexicalProfile

Spanish (Indo-European, Romance). Distinct hand/arm (mano vs brazo) and finger/hand (dedo vs mano). 6 non-derived, 11 total colour categories. Green (verde) and blue (azul) distinct. M-T paradigmatic (me/te). Tea from te. Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.russian : LexicalProfile

Russian (Indo-European, Slavic). Ruka covers both 'hand' and 'arm' (identical). Distinct finger (palec) and hand (ruka). 6 non-derived colour categories; 11 total basic colours (Russian famously distinguishes sinij 'dark blue' from goluboj 'light blue', but WALS counts both). Green (zelenyj) and blue (sinij) distinct. M-T paradigmatic (menja/tebja). Tea from cha (chaj). Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.japanese : LexicalProfile

Japanese (Japonic). Te covers both 'hand' and 'arm' (identical). Distinct finger (yubi) and hand (te). 6 non-derived, 11 total colour categories. Green (midori) and blue (ao) are distinct in modern Japanese (though ao historically covered both). Red (aka) and yellow (kiiro) distinct. No M-T pattern. Tea from cha. Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.mandarin : LexicalProfile

Mandarin Chinese (Sino-Tibetan). Distinct hand/arm (shou vs bei/gebo) and finger/hand. 6 non-derived colour categories; 8--8.5 total basic colours. Green (lu) and blue (lan) distinct. Red (hong) and yellow (huang) distinct. No M-T pattern; no /m/ in 1SG (wo). Tea from cha.

Equations

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

def Phenomena.LexicalTypology.Typology.korean : LexicalProfile

Korean (Koreanic). Distinct hand/arm and finger/hand. 6 non-derived, 11 total colour categories. Green and blue distinct. No M-T pattern. Tea from cha. Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.turkish : LexicalProfile

Turkish (Turkic). Distinct hand/arm (el vs kol) and finger/hand (parmak vs el). M-T paradigmatic (ben/sen with older forms showing m/t). Tea from cha (cay). Clicks used for logical meanings (tongue-click for negation).

Equations

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

def Phenomena.LexicalTypology.Typology.finnish : LexicalProfile

Finnish (Uralic). Distinct hand/arm (kasi vs kasivarsi) and finger/hand (sormi vs kasi). M-T paradigmatic (mina/sina). Tea from te (tee). Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.hungarian : LexicalProfile

Hungarian (Uralic). Distinct hand/arm (kez vs kar) and finger/hand (ujj vs kez). M-T paradigmatic (like Finnish). Tea from te. Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.hindi : LexicalProfile

Hindi (Indo-European, Indo-Aryan). M-T paradigmatic (main/tum show m/t). 1SG has /m/ (main). Tea from cha (chai). Clicks used for logical meanings (tongue-click for negation in many South Asian languages).

Equations

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

def Phenomena.LexicalTypology.Typology.arabic : LexicalProfile

Arabic (Egyptian) (Afro-Asiatic, Semitic). No M-T pattern; no /m/ in 1SG (ana). Tea from cha (shay).

Equations

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

def Phenomena.LexicalTypology.Typology.swahili : LexicalProfile

Swahili (Niger-Congo, Bantu). Mkono covers both 'hand' and 'arm' (identical). Distinct finger/hand. No M-T pattern; 1SG has /m/ (mimi). Tea from cha. Clicks affective.

Equations

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

def Phenomena.LexicalTypology.Typology.tagalog : LexicalProfile

Tagalog (Austronesian). Distinct hand/arm and finger/hand. No M-T pattern. Tea from cha. Clicks: other/none.

Equations

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

def Phenomena.LexicalTypology.Typology.allLanguages : List LexicalProfile

All language profiles in the sample.

Equations

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

theorem Phenomena.LexicalTypology.Typology.wals_f129a_total : Phenomena.LexicalTypology.Typology.ch129✝.length = 617

theorem Phenomena.LexicalTypology.Typology.wals_f130a_total : Phenomena.LexicalTypology.Typology.ch130✝.length = 593

theorem Phenomena.LexicalTypology.Typology.wals_f130b_total : Phenomena.LexicalTypology.Typology.ch130b✝.length = 72

theorem Phenomena.LexicalTypology.Typology.wals_f132a_total : Phenomena.LexicalTypology.Typology.ch132✝.length = 119

theorem Phenomena.LexicalTypology.Typology.wals_f133a_total : Phenomena.LexicalTypology.Typology.ch133✝.length = 119

theorem Phenomena.LexicalTypology.Typology.wals_f134a_total : Phenomena.LexicalTypology.Typology.ch134✝.length = 120

theorem Phenomena.LexicalTypology.Typology.wals_f135a_total : Phenomena.LexicalTypology.Typology.ch135✝.length = 120

theorem Phenomena.LexicalTypology.Typology.wals_f136a_total : Phenomena.LexicalTypology.Typology.ch136a✝.length = 230

theorem Phenomena.LexicalTypology.Typology.wals_f136b_total : Phenomena.LexicalTypology.Typology.ch136b✝.length = 230

theorem Phenomena.LexicalTypology.Typology.wals_f137a_total : Phenomena.LexicalTypology.Typology.ch137a✝.length = 230

theorem Phenomena.LexicalTypology.Typology.wals_f137b_total : Phenomena.LexicalTypology.Typology.ch137b✝.length = 230

theorem Phenomena.LexicalTypology.Typology.wals_f138a_total : Phenomena.LexicalTypology.Typology.ch138✝.length = 230

theorem Phenomena.LexicalTypology.Typology.wals_f139a_total : Phenomena.LexicalTypology.Typology.ch139✝.length = 35

theorem Phenomena.LexicalTypology.Typology.wals_f140a_total : Phenomena.LexicalTypology.Typology.ch140✝.length = 38

theorem Phenomena.LexicalTypology.Typology.wals_f141a_total : Phenomena.LexicalTypology.Typology.ch141✝.length = 6

theorem Phenomena.LexicalTypology.Typology.wals_f142a_total : Phenomena.LexicalTypology.Typology.ch142✝.length = 143

theorem Phenomena.LexicalTypology.Typology.wals_f129a_identical : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => x.value == Core.WALS.F129A.HandAndArm.identical) Phenomena.LexicalTypology.Typology.ch129✝).length = 228

theorem Phenomena.LexicalTypology.Typology.wals_f129a_different : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => x.value == Core.WALS.F129A.HandAndArm.different) Phenomena.LexicalTypology.Typology.ch129✝).length = 389

theorem Phenomena.LexicalTypology.Typology.wals_f130a_identical : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => x.value == Core.WALS.F130A.FingerAndHand.identical) Phenomena.LexicalTypology.Typology.ch130✝).length = 72

theorem Phenomena.LexicalTypology.Typology.wals_f130a_different : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => x.value == Core.WALS.F130A.FingerAndHand.different) Phenomena.LexicalTypology.Typology.ch130✝).length = 521

theorem Phenomena.LexicalTypology.Typology.wals_f130b_hunters : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F130B.CulturalCategoriesOfLanguagesWithIdentityOfFingerAndHand) => x.value == Core.WALS.F130B.CulturalCategoriesOfLanguagesWithIdentityOfFingerAndHand.hunterGatherers) Phenomena.LexicalTypology.Typology.ch130b✝).length = 46

theorem Phenomena.LexicalTypology.Typology.wals_f130b_farmerForagers : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F130B.CulturalCategoriesOfLanguagesWithIdentityOfFingerAndHand) => x.value == Core.WALS.F130B.CulturalCategoriesOfLanguagesWithIdentityOfFingerAndHand.farmerForagers) Phenomena.LexicalTypology.Typology.ch130b✝).length = 18

theorem Phenomena.LexicalTypology.Typology.wals_f130b_farmers : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F130B.CulturalCategoriesOfLanguagesWithIdentityOfFingerAndHand) => x.value == Core.WALS.F130B.CulturalCategoriesOfLanguagesWithIdentityOfFingerAndHand.fullFledgedFarmers) Phenomena.LexicalTypology.Typology.ch130b✝).length = 8

theorem Phenomena.LexicalTypology.Typology.wals_f134a_distinct : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => x.value == Core.WALS.F134A.GreenAndBlue.greenVsBlue) Phenomena.LexicalTypology.Typology.ch134✝).length = 30

theorem Phenomena.LexicalTypology.Typology.wals_f134a_merged : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => x.value == Core.WALS.F134A.GreenAndBlue.greenBlue) Phenomena.LexicalTypology.Typology.ch134✝).length = 68

theorem Phenomena.LexicalTypology.Typology.wals_f135a_distinct : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => x.value == Core.WALS.F135A.RedAndYellow.redVsYellow) Phenomena.LexicalTypology.Typology.ch135✝).length = 98

theorem Phenomena.LexicalTypology.Typology.wals_f135a_merged : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => x.value == Core.WALS.F135A.RedAndYellow.redYellow) Phenomena.LexicalTypology.Typology.ch135✝).length = 15

theorem Phenomena.LexicalTypology.Typology.wals_f136a_absent : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => x.value == Core.WALS.F136A.MTPronouns.noMTPronouns) Phenomena.LexicalTypology.Typology.ch136a✝).length = 200

theorem Phenomena.LexicalTypology.Typology.wals_f136a_paradigmatic : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => x.value == Core.WALS.F136A.MTPronouns.mTPronounsParadigmatic) Phenomena.LexicalTypology.Typology.ch136a✝).length = 27

theorem Phenomena.LexicalTypology.Typology.wals_f138a_cha : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => x.value == Core.WALS.F138A.Tea.wordsDerivedFromSiniticCha) Phenomena.LexicalTypology.Typology.ch138✝).length = 110

theorem Phenomena.LexicalTypology.Typology.wals_f138a_te : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => x.value == Core.WALS.F138A.Tea.wordsDerivedFromMinNanChineseTe) Phenomena.LexicalTypology.Typology.ch138✝).length = 84

theorem Phenomena.LexicalTypology.Typology.wals_f138a_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => x.value == Core.WALS.F138A.Tea.others) Phenomena.LexicalTypology.Typology.ch138✝).length = 36

theorem Phenomena.LexicalTypology.Typology.wals_f142a_logical : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => x.value == Core.WALS.F142A.ParaLinguisticUsagesOfClicks.logicalMeanings) Phenomena.LexicalTypology.Typology.ch142✝).length = 47

theorem Phenomena.LexicalTypology.Typology.wals_f142a_affective : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => x.value == Core.WALS.F142A.ParaLinguisticUsagesOfClicks.affectiveMeanings) Phenomena.LexicalTypology.Typology.ch142✝).length = 71

theorem Phenomena.LexicalTypology.Typology.wals_f142a_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => x.value == Core.WALS.F142A.ParaLinguisticUsagesOfClicks.otherOrNone) Phenomena.LexicalTypology.Typology.ch142✝).length = 25

theorem Phenomena.LexicalTypology.Typology.sample_size : allLanguages.length = 15

theorem Phenomena.LexicalTypology.Typology.english_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "eng") = english.handArm

theorem Phenomena.LexicalTypology.Typology.french_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "fre") = french.handArm

theorem Phenomena.LexicalTypology.Typology.german_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "ger") = german.handArm

theorem Phenomena.LexicalTypology.Typology.spanish_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "spa") = spanish.handArm

theorem Phenomena.LexicalTypology.Typology.russian_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "rus") = russian.handArm

theorem Phenomena.LexicalTypology.Typology.japanese_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "jpn") = japanese.handArm

theorem Phenomena.LexicalTypology.Typology.mandarin_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "mnd") = mandarin.handArm

theorem Phenomena.LexicalTypology.Typology.korean_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "kor") = korean.handArm

theorem Phenomena.LexicalTypology.Typology.turkish_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "tur") = turkish.handArm

theorem Phenomena.LexicalTypology.Typology.finnish_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "fin") = finnish.handArm

theorem Phenomena.LexicalTypology.Typology.hungarian_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "hun") = hungarian.handArm

theorem Phenomena.LexicalTypology.Typology.swahili_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "swa") = swahili.handArm

theorem Phenomena.LexicalTypology.Typology.tagalog_f129a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F129A.HandAndArm) => Phenomena.LexicalTypology.Typology.fromWALS129A✝ x.value) (Core.WALS.F129A.lookup "tag") = tagalog.handArm

theorem Phenomena.LexicalTypology.Typology.english_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "eng") = english.fingerHand

theorem Phenomena.LexicalTypology.Typology.french_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "fre") = french.fingerHand

theorem Phenomena.LexicalTypology.Typology.german_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "ger") = german.fingerHand

theorem Phenomena.LexicalTypology.Typology.spanish_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "spa") = spanish.fingerHand

theorem Phenomena.LexicalTypology.Typology.russian_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "rus") = russian.fingerHand

theorem Phenomena.LexicalTypology.Typology.japanese_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "jpn") = japanese.fingerHand

theorem Phenomena.LexicalTypology.Typology.mandarin_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "mnd") = mandarin.fingerHand

theorem Phenomena.LexicalTypology.Typology.korean_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "kor") = korean.fingerHand

theorem Phenomena.LexicalTypology.Typology.turkish_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "tur") = turkish.fingerHand

theorem Phenomena.LexicalTypology.Typology.finnish_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "fin") = finnish.fingerHand

theorem Phenomena.LexicalTypology.Typology.hungarian_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "hun") = hungarian.fingerHand

theorem Phenomena.LexicalTypology.Typology.swahili_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "swa") = swahili.fingerHand

theorem Phenomena.LexicalTypology.Typology.tagalog_f130a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F130A.FingerAndHand) => Phenomena.LexicalTypology.Typology.fromWALS130A✝ x.value) (Core.WALS.F130A.lookup "tag") = tagalog.fingerHand

theorem Phenomena.LexicalTypology.Typology.english_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "eng") = english.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.french_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "fre") = french.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.german_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "ger") = german.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.spanish_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "spa") = spanish.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.russian_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "rus") = russian.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.japanese_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "jpn") = japanese.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.mandarin_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "mnd") = mandarin.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.korean_f132a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F132A.NumberOfNonDerivedBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS132A✝ x.value) (Core.WALS.F132A.lookup "kor") = korean.nonDerivedColours

theorem Phenomena.LexicalTypology.Typology.english_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "eng") = english.basicColours

theorem Phenomena.LexicalTypology.Typology.french_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "fre") = french.basicColours

theorem Phenomena.LexicalTypology.Typology.german_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "ger") = german.basicColours

theorem Phenomena.LexicalTypology.Typology.spanish_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "spa") = spanish.basicColours

theorem Phenomena.LexicalTypology.Typology.russian_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "rus") = russian.basicColours

theorem Phenomena.LexicalTypology.Typology.japanese_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "jpn") = japanese.basicColours

theorem Phenomena.LexicalTypology.Typology.mandarin_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "mnd") = mandarin.basicColours

theorem Phenomena.LexicalTypology.Typology.korean_f133a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F133A.NumberOfBasicColourCategories) => Phenomena.LexicalTypology.Typology.fromWALS133A✝ x.value) (Core.WALS.F133A.lookup "kor") = korean.basicColours

theorem Phenomena.LexicalTypology.Typology.english_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "eng") = english.greenBlue

theorem Phenomena.LexicalTypology.Typology.french_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "fre") = french.greenBlue

theorem Phenomena.LexicalTypology.Typology.german_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "ger") = german.greenBlue

theorem Phenomena.LexicalTypology.Typology.spanish_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "spa") = spanish.greenBlue

theorem Phenomena.LexicalTypology.Typology.russian_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "rus") = russian.greenBlue

theorem Phenomena.LexicalTypology.Typology.japanese_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "jpn") = japanese.greenBlue

theorem Phenomena.LexicalTypology.Typology.mandarin_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "mnd") = mandarin.greenBlue

theorem Phenomena.LexicalTypology.Typology.korean_f134a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F134A.GreenAndBlue) => Phenomena.LexicalTypology.Typology.fromWALS134A✝ x.value) (Core.WALS.F134A.lookup "kor") = korean.greenBlue

theorem Phenomena.LexicalTypology.Typology.english_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "eng") = english.redYellow

theorem Phenomena.LexicalTypology.Typology.french_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "fre") = french.redYellow

theorem Phenomena.LexicalTypology.Typology.german_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "ger") = german.redYellow

theorem Phenomena.LexicalTypology.Typology.spanish_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "spa") = spanish.redYellow

theorem Phenomena.LexicalTypology.Typology.russian_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "rus") = russian.redYellow

theorem Phenomena.LexicalTypology.Typology.japanese_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "jpn") = japanese.redYellow

theorem Phenomena.LexicalTypology.Typology.mandarin_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "mnd") = mandarin.redYellow

theorem Phenomena.LexicalTypology.Typology.korean_f135a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F135A.RedAndYellow) => Phenomena.LexicalTypology.Typology.fromWALS135A✝ x.value) (Core.WALS.F135A.lookup "kor") = korean.redYellow

theorem Phenomena.LexicalTypology.Typology.english_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "eng") = english.mtPronouns

theorem Phenomena.LexicalTypology.Typology.french_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "fre") = french.mtPronouns

theorem Phenomena.LexicalTypology.Typology.german_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "ger") = german.mtPronouns

theorem Phenomena.LexicalTypology.Typology.spanish_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "spa") = spanish.mtPronouns

theorem Phenomena.LexicalTypology.Typology.russian_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "rus") = russian.mtPronouns

theorem Phenomena.LexicalTypology.Typology.japanese_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "jpn") = japanese.mtPronouns

theorem Phenomena.LexicalTypology.Typology.mandarin_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "mnd") = mandarin.mtPronouns

theorem Phenomena.LexicalTypology.Typology.korean_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "kor") = korean.mtPronouns

theorem Phenomena.LexicalTypology.Typology.turkish_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "tur") = turkish.mtPronouns

theorem Phenomena.LexicalTypology.Typology.finnish_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "fin") = finnish.mtPronouns

theorem Phenomena.LexicalTypology.Typology.hungarian_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "hun") = hungarian.mtPronouns

theorem Phenomena.LexicalTypology.Typology.hindi_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "hin") = hindi.mtPronouns

theorem Phenomena.LexicalTypology.Typology.arabic_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "aeg") = arabic.mtPronouns

theorem Phenomena.LexicalTypology.Typology.swahili_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "swa") = swahili.mtPronouns

theorem Phenomena.LexicalTypology.Typology.tagalog_f136a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136A.MTPronouns) => Phenomena.LexicalTypology.Typology.fromWALS136A✝ x.value) (Core.WALS.F136A.lookup "tag") = tagalog.mtPronouns

theorem Phenomena.LexicalTypology.Typology.english_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "eng") = english.mIn1sg

theorem Phenomena.LexicalTypology.Typology.french_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "fre") = french.mIn1sg

theorem Phenomena.LexicalTypology.Typology.german_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "ger") = german.mIn1sg

theorem Phenomena.LexicalTypology.Typology.spanish_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "spa") = spanish.mIn1sg

theorem Phenomena.LexicalTypology.Typology.russian_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "rus") = russian.mIn1sg

theorem Phenomena.LexicalTypology.Typology.japanese_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "jpn") = japanese.mIn1sg

theorem Phenomena.LexicalTypology.Typology.mandarin_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "mnd") = mandarin.mIn1sg

theorem Phenomena.LexicalTypology.Typology.korean_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "kor") = korean.mIn1sg

theorem Phenomena.LexicalTypology.Typology.turkish_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "tur") = turkish.mIn1sg

theorem Phenomena.LexicalTypology.Typology.finnish_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "fin") = finnish.mIn1sg

theorem Phenomena.LexicalTypology.Typology.hungarian_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "hun") = hungarian.mIn1sg

theorem Phenomena.LexicalTypology.Typology.hindi_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "hin") = hindi.mIn1sg

theorem Phenomena.LexicalTypology.Typology.arabic_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "aeg") = arabic.mIn1sg

theorem Phenomena.LexicalTypology.Typology.swahili_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "swa") = swahili.mIn1sg

theorem Phenomena.LexicalTypology.Typology.tagalog_f136b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F136B.MInFirstPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS136B✝ x.value) (Core.WALS.F136B.lookup "tag") = tagalog.mIn1sg

theorem Phenomena.LexicalTypology.Typology.english_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "eng") = english.nmPronouns

theorem Phenomena.LexicalTypology.Typology.french_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "fre") = french.nmPronouns

theorem Phenomena.LexicalTypology.Typology.german_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "ger") = german.nmPronouns

theorem Phenomena.LexicalTypology.Typology.spanish_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "spa") = spanish.nmPronouns

theorem Phenomena.LexicalTypology.Typology.russian_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "rus") = russian.nmPronouns

theorem Phenomena.LexicalTypology.Typology.japanese_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "jpn") = japanese.nmPronouns

theorem Phenomena.LexicalTypology.Typology.mandarin_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "mnd") = mandarin.nmPronouns

theorem Phenomena.LexicalTypology.Typology.korean_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "kor") = korean.nmPronouns

theorem Phenomena.LexicalTypology.Typology.turkish_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "tur") = turkish.nmPronouns

theorem Phenomena.LexicalTypology.Typology.finnish_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "fin") = finnish.nmPronouns

theorem Phenomena.LexicalTypology.Typology.hungarian_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "hun") = hungarian.nmPronouns

theorem Phenomena.LexicalTypology.Typology.hindi_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "hin") = hindi.nmPronouns

theorem Phenomena.LexicalTypology.Typology.arabic_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "aeg") = arabic.nmPronouns

theorem Phenomena.LexicalTypology.Typology.swahili_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "swa") = swahili.nmPronouns

theorem Phenomena.LexicalTypology.Typology.tagalog_f137a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137A.NMPronouns) => Phenomena.LexicalTypology.Typology.fromWALS137A✝ x.value) (Core.WALS.F137A.lookup "tag") = tagalog.nmPronouns

theorem Phenomena.LexicalTypology.Typology.english_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "eng") = english.mIn2sg

theorem Phenomena.LexicalTypology.Typology.french_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "fre") = french.mIn2sg

theorem Phenomena.LexicalTypology.Typology.german_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "ger") = german.mIn2sg

theorem Phenomena.LexicalTypology.Typology.spanish_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "spa") = spanish.mIn2sg

theorem Phenomena.LexicalTypology.Typology.russian_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "rus") = russian.mIn2sg

theorem Phenomena.LexicalTypology.Typology.japanese_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "jpn") = japanese.mIn2sg

theorem Phenomena.LexicalTypology.Typology.mandarin_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "mnd") = mandarin.mIn2sg

theorem Phenomena.LexicalTypology.Typology.korean_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "kor") = korean.mIn2sg

theorem Phenomena.LexicalTypology.Typology.turkish_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "tur") = turkish.mIn2sg

theorem Phenomena.LexicalTypology.Typology.finnish_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "fin") = finnish.mIn2sg

theorem Phenomena.LexicalTypology.Typology.hungarian_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "hun") = hungarian.mIn2sg

theorem Phenomena.LexicalTypology.Typology.hindi_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "hin") = hindi.mIn2sg

theorem Phenomena.LexicalTypology.Typology.arabic_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "aeg") = arabic.mIn2sg

theorem Phenomena.LexicalTypology.Typology.swahili_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "swa") = swahili.mIn2sg

theorem Phenomena.LexicalTypology.Typology.tagalog_f137b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F137B.MInSecondPersonSingular) => Phenomena.LexicalTypology.Typology.fromWALS137B✝ x.value) (Core.WALS.F137B.lookup "tag") = tagalog.mIn2sg

theorem Phenomena.LexicalTypology.Typology.english_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "eng") = english.tea

theorem Phenomena.LexicalTypology.Typology.french_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "fre") = french.tea

theorem Phenomena.LexicalTypology.Typology.german_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "ger") = german.tea

theorem Phenomena.LexicalTypology.Typology.spanish_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "spa") = spanish.tea

theorem Phenomena.LexicalTypology.Typology.russian_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "rus") = russian.tea

theorem Phenomena.LexicalTypology.Typology.japanese_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "jpn") = japanese.tea

theorem Phenomena.LexicalTypology.Typology.mandarin_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "mnd") = mandarin.tea

theorem Phenomena.LexicalTypology.Typology.korean_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "kor") = korean.tea

theorem Phenomena.LexicalTypology.Typology.turkish_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "tur") = turkish.tea

theorem Phenomena.LexicalTypology.Typology.finnish_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "fin") = finnish.tea

theorem Phenomena.LexicalTypology.Typology.hungarian_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "hun") = hungarian.tea

theorem Phenomena.LexicalTypology.Typology.hindi_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "hin") = hindi.tea

theorem Phenomena.LexicalTypology.Typology.arabic_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "aeg") = arabic.tea

theorem Phenomena.LexicalTypology.Typology.swahili_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "swa") = swahili.tea

theorem Phenomena.LexicalTypology.Typology.tagalog_f138a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F138A.Tea) => Phenomena.LexicalTypology.Typology.fromWALS138A✝ x.value) (Core.WALS.F138A.lookup "tag") = tagalog.tea

theorem Phenomena.LexicalTypology.Typology.english_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "eng") = english.clicks

theorem Phenomena.LexicalTypology.Typology.german_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "ger") = german.clicks

theorem Phenomena.LexicalTypology.Typology.spanish_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "spa") = spanish.clicks

theorem Phenomena.LexicalTypology.Typology.russian_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "rus") = russian.clicks

theorem Phenomena.LexicalTypology.Typology.japanese_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "jpn") = japanese.clicks

theorem Phenomena.LexicalTypology.Typology.korean_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "kor") = korean.clicks

theorem Phenomena.LexicalTypology.Typology.turkish_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "tur") = turkish.clicks

theorem Phenomena.LexicalTypology.Typology.finnish_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "fin") = finnish.clicks

theorem Phenomena.LexicalTypology.Typology.hungarian_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "hun") = hungarian.clicks

theorem Phenomena.LexicalTypology.Typology.hindi_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "hin") = hindi.clicks

theorem Phenomena.LexicalTypology.Typology.swahili_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "swa") = swahili.clicks

theorem Phenomena.LexicalTypology.Typology.tagalog_f142a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F142A.ParaLinguisticUsagesOfClicks) => Phenomena.LexicalTypology.Typology.fromWALS142A✝ x.value) (Core.WALS.F142A.lookup "tag") = tagalog.clicks

theorem Phenomena.LexicalTypology.Typology.hand_arm_different_majority : 389 > 228

Most languages distinguish 'hand' from 'arm' (389 vs 228).

theorem Phenomena.LexicalTypology.Typology.finger_hand_identity_rare : 72 * 8 < 593

Finger-hand identity is rare: only 72/593 = 12% of languages.

theorem Phenomena.LexicalTypology.Typology.finger_hand_hunter_gatherer_majority : 46 * 2 > 72

Among languages with finger=hand identity, hunter-gatherers dominate (46/72 = 64%).

theorem Phenomena.LexicalTypology.Typology.grue_majority : 68 > 30

Grue (merged green/blue) is the majority pattern for the green-blue dimension (68/120 = 57%), far exceeding the distinct-terms pattern (30).

theorem Phenomena.LexicalTypology.Typology.red_yellow_usually_distinct : 98 * 5 > 120 * 4

Red and yellow are almost always distinguished: 98/120 = 82% of languages have separate terms.

theorem Phenomena.LexicalTypology.Typology.mt_pronouns_minority : 200 > 30

The M-T pronoun pattern is a minority pattern: only 30/230 languages show any form of it. Most languages (200/230) lack it.

theorem Phenomena.LexicalTypology.Typology.cha_more_common_than_te : 110 > 84

The cha route for tea is slightly more common than te: 110 vs 84 languages. Both vastly outnumber independent forms (36).

theorem Phenomena.LexicalTypology.Typology.tea_wanderwort_dominant : 110 + 84 > 36 * 5

theorem Phenomena.LexicalTypology.Typology.affective_clicks_more_common : 71 > 47

Affective click usage is more common than logical click usage (71 vs 47 languages).

theorem Phenomena.LexicalTypology.Typology.mt_implies_m_in_1sg : (allLanguages.all fun (p : LexicalProfile) => match p.mtPronouns, p.mIn1sg with | some MTPronounPattern.paradigmatic, some v => v == MIn1SG.present | x, x_1 => true) = true

In our sample, all European languages with an M-T pattern also have /m/ in 1SG (expected, since the M-T pattern implies 1SG=m).

def Phenomena.LexicalTypology.Typology.chaLanguages : List LexicalProfile

The cha/te split in our sample follows geography: East/South Asian + Russian languages use cha, while Western European languages use te.

Equations

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

def Phenomena.LexicalTypology.Typology.teLanguages : List LexicalProfile

Equations

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

theorem Phenomena.LexicalTypology.Typology.cha_language_count : chaLanguages.length = 9

theorem Phenomena.LexicalTypology.Typology.te_language_count : teLanguages.length = 6

theorem Phenomena.LexicalTypology.Typology.all_sampled_have_six_nonderived : (allLanguages.all fun (p : LexicalProfile) => match p.nonDerivedColours with | some v => v == NonDerivedColourCount.six | none => true) = true

All languages in our sample with colour data have exactly 6 non-derived basic colour categories.

theorem Phenomena.LexicalTypology.Typology.all_sampled_distinguish_green_blue : (allLanguages.all fun (p : LexicalProfile) => match p.greenBlue with | some v => v == GreenBlueRelation.distinct | none => true) = true

All languages in our sample with colour data distinguish green from blue (no grue languages in our major-language sample).