Phonological Typology (WALS Chapters 1--19)

@cite{dryer-haspelmath-2013} @cite{maddieson-2013}

Formalizes the phonological inventory and prosodic typology chapters from the World Atlas of Language Structures (WALS), covering:

• Segmental inventory (Ch 1--8, 18--19): Consonant and vowel inventory size, consonant-to-vowel ratio, voicing contrasts, and the presence/absence of specific consonant types (uvulars, glottalized consonants, laterals, the velar nasal, uncommon consonants like clicks and labial-velars).

• Vowel features (Ch 10--11): Vowel nasalization contrasts, nasal vowels in West Africa (Ch 10B), and front rounded vowels.

• Syllable structure (Ch 12): Simple, moderately complex, or complex.

• Prosody (Ch 13--17): Tone systems, fixed vs. free stress location, weight-sensitive stress (Ch 15A), weight factors (Ch 16A), and rhythmic type (trochaic vs. iambic).

The 19 WALS features are captured in a single PhonProfile structure. Chapters 5, 10B, 15, and 16 are omitted from the profile as they are sub-classifications of other chapters, but their generated data is available via converter functions, grounding theorems, and distribution theorems.

inductive Phenomena.Phonology.CInventorySize : Type

Consonant inventory size (WALS Ch 1).

• small : CInventorySize
• moderatelySmall : CInventorySize
• average : CInventorySize
• moderatelyLarge : CInventorySize
• large : CInventorySize

instance Phenomena.Phonology.instDecidableEqCInventorySize : DecidableEq CInventorySize

Equations

• Phenomena.Phonology.instDecidableEqCInventorySize x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqCInventorySize : BEq CInventorySize

Equations

• Phenomena.Phonology.instBEqCInventorySize = { beq := Phenomena.Phonology.instBEqCInventorySize.beq }

def Phenomena.Phonology.instBEqCInventorySize.beq : CInventorySize → CInventorySize → Bool

Equations

• Phenomena.Phonology.instBEqCInventorySize.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Phonology.instReprCInventorySize.repr : CInventorySize → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprCInventorySize : Repr CInventorySize

Equations

• Phenomena.Phonology.instReprCInventorySize = { reprPrec := Phenomena.Phonology.instReprCInventorySize.repr }

inductive Phenomena.Phonology.VInventorySize : Type

Vowel quality inventory size (WALS Ch 2).

• small : VInventorySize
• average : VInventorySize
• large : VInventorySize

instance Phenomena.Phonology.instDecidableEqVInventorySize : DecidableEq VInventorySize

Equations

• Phenomena.Phonology.instDecidableEqVInventorySize x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqVInventorySize.beq : VInventorySize → VInventorySize → Bool

Equations

• Phenomena.Phonology.instBEqVInventorySize.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqVInventorySize : BEq VInventorySize

Equations

• Phenomena.Phonology.instBEqVInventorySize = { beq := Phenomena.Phonology.instBEqVInventorySize.beq }

def Phenomena.Phonology.instReprVInventorySize.repr : VInventorySize → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprVInventorySize : Repr VInventorySize

Equations

• Phenomena.Phonology.instReprVInventorySize = { reprPrec := Phenomena.Phonology.instReprVInventorySize.repr }

inductive Phenomena.Phonology.CVRatio : Type

Consonant-to-vowel ratio (WALS Ch 3).

• low : CVRatio
• moderatelyLow : CVRatio
• average : CVRatio
• moderatelyHigh : CVRatio
• high : CVRatio

instance Phenomena.Phonology.instDecidableEqCVRatio : DecidableEq CVRatio

Equations

• Phenomena.Phonology.instDecidableEqCVRatio x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqCVRatio : BEq CVRatio

Equations

• Phenomena.Phonology.instBEqCVRatio = { beq := Phenomena.Phonology.instBEqCVRatio.beq }

def Phenomena.Phonology.instBEqCVRatio.beq : CVRatio → CVRatio → Bool

Equations

• Phenomena.Phonology.instBEqCVRatio.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Phonology.instReprCVRatio.repr : CVRatio → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprCVRatio : Repr CVRatio

Equations

• Phenomena.Phonology.instReprCVRatio = { reprPrec := Phenomena.Phonology.instReprCVRatio.repr }

inductive Phenomena.Phonology.VoicingContrast : Type

Voicing contrast in obstruents (WALS Ch 4).

• none : VoicingContrast
• plosivesOnly : VoicingContrast
• fricativesOnly : VoicingContrast
• both : VoicingContrast

instance Phenomena.Phonology.instDecidableEqVoicingContrast : DecidableEq VoicingContrast

Equations

• Phenomena.Phonology.instDecidableEqVoicingContrast x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqVoicingContrast.beq : VoicingContrast → VoicingContrast → Bool

Equations

• Phenomena.Phonology.instBEqVoicingContrast.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqVoicingContrast : BEq VoicingContrast

Equations

• Phenomena.Phonology.instBEqVoicingContrast = { beq := Phenomena.Phonology.instBEqVoicingContrast.beq }

instance Phenomena.Phonology.instReprVoicingContrast : Repr VoicingContrast

Equations

• Phenomena.Phonology.instReprVoicingContrast = { reprPrec := Phenomena.Phonology.instReprVoicingContrast.repr }

def Phenomena.Phonology.instReprVoicingContrast.repr : VoicingContrast → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.UvularPresence : Type

Uvular consonant inventory (WALS Ch 6).

• none : UvularPresence
• stopsOnly : UvularPresence
• continuantsOnly : UvularPresence
• stopsAndContinuants : UvularPresence

instance Phenomena.Phonology.instDecidableEqUvularPresence : DecidableEq UvularPresence

Equations

• Phenomena.Phonology.instDecidableEqUvularPresence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqUvularPresence.beq : UvularPresence → UvularPresence → Bool

Equations

• Phenomena.Phonology.instBEqUvularPresence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqUvularPresence : BEq UvularPresence

Equations

• Phenomena.Phonology.instBEqUvularPresence = { beq := Phenomena.Phonology.instBEqUvularPresence.beq }

def Phenomena.Phonology.instReprUvularPresence.repr : UvularPresence → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprUvularPresence : Repr UvularPresence

Equations

• Phenomena.Phonology.instReprUvularPresence = { reprPrec := Phenomena.Phonology.instReprUvularPresence.repr }

inductive Phenomena.Phonology.GlottalizedType : Type

Glottalized consonant types (WALS Ch 7).

• none : GlottalizedType
• ejectivesOnly : GlottalizedType
• implosivesOnly : GlottalizedType
• resonantsOnly : GlottalizedType
• ejectivesAndImplosives : GlottalizedType
• ejectivesAndResonants : GlottalizedType
• implosivesAndResonants : GlottalizedType
• allThree : GlottalizedType

instance Phenomena.Phonology.instDecidableEqGlottalizedType : DecidableEq GlottalizedType

Equations

• Phenomena.Phonology.instDecidableEqGlottalizedType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqGlottalizedType : BEq GlottalizedType

Equations

• Phenomena.Phonology.instBEqGlottalizedType = { beq := Phenomena.Phonology.instBEqGlottalizedType.beq }

def Phenomena.Phonology.instBEqGlottalizedType.beq : GlottalizedType → GlottalizedType → Bool

Equations

• Phenomena.Phonology.instBEqGlottalizedType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instReprGlottalizedType : Repr GlottalizedType

Equations

• Phenomena.Phonology.instReprGlottalizedType = { reprPrec := Phenomena.Phonology.instReprGlottalizedType.repr }

def Phenomena.Phonology.instReprGlottalizedType.repr : GlottalizedType → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.LateralType : Type

Lateral consonant inventory (WALS Ch 8).

• noLaterals : LateralType
• lOnly : LateralType
• lateralsNoL : LateralType
• lAndObstruent : LateralType
• obstruentOnly : LateralType

instance Phenomena.Phonology.instDecidableEqLateralType : DecidableEq LateralType

Equations

• Phenomena.Phonology.instDecidableEqLateralType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqLateralType : BEq LateralType

Equations

• Phenomena.Phonology.instBEqLateralType = { beq := Phenomena.Phonology.instBEqLateralType.beq }

def Phenomena.Phonology.instBEqLateralType.beq : LateralType → LateralType → Bool

Equations

• Phenomena.Phonology.instBEqLateralType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Phonology.instReprLateralType.repr : LateralType → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprLateralType : Repr LateralType

Equations

• Phenomena.Phonology.instReprLateralType = { reprPrec := Phenomena.Phonology.instReprLateralType.repr }

inductive Phenomena.Phonology.VelarNasalStatus : Type

Velar nasal status (WALS Ch 9).

• initial : VelarNasalStatus
• noInitial : VelarNasalStatus
• absent : VelarNasalStatus

instance Phenomena.Phonology.instDecidableEqVelarNasalStatus : DecidableEq VelarNasalStatus

Equations

• Phenomena.Phonology.instDecidableEqVelarNasalStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqVelarNasalStatus : BEq VelarNasalStatus

Equations

• Phenomena.Phonology.instBEqVelarNasalStatus = { beq := Phenomena.Phonology.instBEqVelarNasalStatus.beq }

def Phenomena.Phonology.instBEqVelarNasalStatus.beq : VelarNasalStatus → VelarNasalStatus → Bool

Equations

• Phenomena.Phonology.instBEqVelarNasalStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Phonology.instReprVelarNasalStatus.repr : VelarNasalStatus → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprVelarNasalStatus : Repr VelarNasalStatus

Equations

• Phenomena.Phonology.instReprVelarNasalStatus = { reprPrec := Phenomena.Phonology.instReprVelarNasalStatus.repr }

inductive Phenomena.Phonology.NasalVowelWA : Type

Nasal vowel contrast type in West Africa (WALS Ch 10B). Areal sub-feature of Ch 10A, covering 40 West African languages.

• noContrast : NasalVowelWA
• twoWayNoSpreading : NasalVowelWA
• twoWaySpreading : NasalVowelWA
• fourWayNoSpreading : NasalVowelWA
• fourWaySpreading : NasalVowelWA

instance Phenomena.Phonology.instDecidableEqNasalVowelWA : DecidableEq NasalVowelWA

Equations

• Phenomena.Phonology.instDecidableEqNasalVowelWA x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqNasalVowelWA.beq : NasalVowelWA → NasalVowelWA → Bool

Equations

• Phenomena.Phonology.instBEqNasalVowelWA.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqNasalVowelWA : BEq NasalVowelWA

Equations

• Phenomena.Phonology.instBEqNasalVowelWA = { beq := Phenomena.Phonology.instBEqNasalVowelWA.beq }

instance Phenomena.Phonology.instReprNasalVowelWA : Repr NasalVowelWA

Equations

• Phenomena.Phonology.instReprNasalVowelWA = { reprPrec := Phenomena.Phonology.instReprNasalVowelWA.repr }

def Phenomena.Phonology.instReprNasalVowelWA.repr : NasalVowelWA → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.FrontRounded : Type

Front rounded vowel inventory (WALS Ch 11).

• none : FrontRounded
• highAndMid : FrontRounded
• highOnly : FrontRounded
• midOnly : FrontRounded

instance Phenomena.Phonology.instDecidableEqFrontRounded : DecidableEq FrontRounded

Equations

• Phenomena.Phonology.instDecidableEqFrontRounded x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqFrontRounded : BEq FrontRounded

Equations

• Phenomena.Phonology.instBEqFrontRounded = { beq := Phenomena.Phonology.instBEqFrontRounded.beq }

def Phenomena.Phonology.instBEqFrontRounded.beq : FrontRounded → FrontRounded → Bool

Equations

• Phenomena.Phonology.instBEqFrontRounded.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instReprFrontRounded : Repr FrontRounded

Equations

• Phenomena.Phonology.instReprFrontRounded = { reprPrec := Phenomena.Phonology.instReprFrontRounded.repr }

def Phenomena.Phonology.instReprFrontRounded.repr : FrontRounded → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.SyllableComplexity : Type

Syllable structure complexity (WALS Ch 12).

• simple : SyllableComplexity
• moderatelyComplex : SyllableComplexity
• complex : SyllableComplexity

instance Phenomena.Phonology.instDecidableEqSyllableComplexity : DecidableEq SyllableComplexity

Equations

• Phenomena.Phonology.instDecidableEqSyllableComplexity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqSyllableComplexity : BEq SyllableComplexity

Equations

• Phenomena.Phonology.instBEqSyllableComplexity = { beq := Phenomena.Phonology.instBEqSyllableComplexity.beq }

def Phenomena.Phonology.instBEqSyllableComplexity.beq : SyllableComplexity → SyllableComplexity → Bool

Equations

• Phenomena.Phonology.instBEqSyllableComplexity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instReprSyllableComplexity : Repr SyllableComplexity

Equations

• Phenomena.Phonology.instReprSyllableComplexity = { reprPrec := Phenomena.Phonology.instReprSyllableComplexity.repr }

def Phenomena.Phonology.instReprSyllableComplexity.repr : SyllableComplexity → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.ToneSystem : Type

Tone system type (WALS Ch 13).

• none : ToneSystem
• simple : ToneSystem
• complex : ToneSystem

instance Phenomena.Phonology.instDecidableEqToneSystem : DecidableEq ToneSystem

Equations

• Phenomena.Phonology.instDecidableEqToneSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqToneSystem.beq : ToneSystem → ToneSystem → Bool

Equations

• Phenomena.Phonology.instBEqToneSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqToneSystem : BEq ToneSystem

Equations

• Phenomena.Phonology.instBEqToneSystem = { beq := Phenomena.Phonology.instBEqToneSystem.beq }

instance Phenomena.Phonology.instReprToneSystem : Repr ToneSystem

Equations

• Phenomena.Phonology.instReprToneSystem = { reprPrec := Phenomena.Phonology.instReprToneSystem.repr }

def Phenomena.Phonology.instReprToneSystem.repr : ToneSystem → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.StressLocation : Type

Fixed stress location (WALS Ch 14).

• noFixed : StressLocation
• initial : StressLocation
• second : StressLocation
• third : StressLocation
• antepenultimate : StressLocation
• penultimate : StressLocation
• ultimate : StressLocation

instance Phenomena.Phonology.instDecidableEqStressLocation : DecidableEq StressLocation

Equations

• Phenomena.Phonology.instDecidableEqStressLocation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqStressLocation.beq : StressLocation → StressLocation → Bool

Equations

• Phenomena.Phonology.instBEqStressLocation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqStressLocation : BEq StressLocation

Equations

• Phenomena.Phonology.instBEqStressLocation = { beq := Phenomena.Phonology.instBEqStressLocation.beq }

instance Phenomena.Phonology.instReprStressLocation : Repr StressLocation

Equations

• Phenomena.Phonology.instReprStressLocation = { reprPrec := Phenomena.Phonology.instReprStressLocation.repr }

def Phenomena.Phonology.instReprStressLocation.repr : StressLocation → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.WeightStress : Type

Weight-sensitive stress pattern (WALS Ch 15A). Sub-feature of Ch 14A, classifying how stress interacts with syllable weight.

• leftEdge : WeightStress
• leftOriented : WeightStress
• rightEdge : WeightStress
• rightOriented : WeightStress
• unbounded : WeightStress
• combinedRightUnbounded : WeightStress
• notPredictable : WeightStress
• fixedNoWeight : WeightStress

instance Phenomena.Phonology.instDecidableEqWeightStress : DecidableEq WeightStress

Equations

• Phenomena.Phonology.instDecidableEqWeightStress x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqWeightStress.beq : WeightStress → WeightStress → Bool

Equations

• Phenomena.Phonology.instBEqWeightStress.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqWeightStress : BEq WeightStress

Equations

• Phenomena.Phonology.instBEqWeightStress = { beq := Phenomena.Phonology.instBEqWeightStress.beq }

instance Phenomena.Phonology.instReprWeightStress : Repr WeightStress

Equations

• Phenomena.Phonology.instReprWeightStress = { reprPrec := Phenomena.Phonology.instReprWeightStress.repr }

def Phenomena.Phonology.instReprWeightStress.repr : WeightStress → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.WeightFactor : Type

Weight factor in weight-sensitive stress (WALS Ch 16A). Sub-feature of Ch 14A, classifying what makes a syllable heavy.

• noWeight : WeightFactor
• longVowel : WeightFactor
• codaConsonant : WeightFactor
• longVowelOrCoda : WeightFactor
• prominence : WeightFactor
• lexicalStress : WeightFactor
• combined : WeightFactor

instance Phenomena.Phonology.instDecidableEqWeightFactor : DecidableEq WeightFactor

Equations

• Phenomena.Phonology.instDecidableEqWeightFactor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqWeightFactor : BEq WeightFactor

Equations

• Phenomena.Phonology.instBEqWeightFactor = { beq := Phenomena.Phonology.instBEqWeightFactor.beq }

def Phenomena.Phonology.instBEqWeightFactor.beq : WeightFactor → WeightFactor → Bool

Equations

• Phenomena.Phonology.instBEqWeightFactor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Phonology.instReprWeightFactor.repr : WeightFactor → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprWeightFactor : Repr WeightFactor

Equations

• Phenomena.Phonology.instReprWeightFactor = { reprPrec := Phenomena.Phonology.instReprWeightFactor.repr }

inductive Phenomena.Phonology.RhythmType : Type

Rhythmic type (WALS Ch 17).

• trochaic : RhythmType
• iambic : RhythmType
• dual : RhythmType
• undetermined : RhythmType
• noRhythm : RhythmType

instance Phenomena.Phonology.instDecidableEqRhythmType : DecidableEq RhythmType

Equations

• Phenomena.Phonology.instDecidableEqRhythmType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Phonology.instBEqRhythmType.beq : RhythmType → RhythmType → Bool

Equations

• Phenomena.Phonology.instBEqRhythmType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instBEqRhythmType : BEq RhythmType

Equations

• Phenomena.Phonology.instBEqRhythmType = { beq := Phenomena.Phonology.instBEqRhythmType.beq }

instance Phenomena.Phonology.instReprRhythmType : Repr RhythmType

Equations

• Phenomena.Phonology.instReprRhythmType = { reprPrec := Phenomena.Phonology.instReprRhythmType.repr }

def Phenomena.Phonology.instReprRhythmType.repr : RhythmType → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.MissingCommon : Type

Missing common consonants (WALS Ch 18).

• allPresent : MissingCommon
• noBilabials : MissingCommon
• noFricatives : MissingCommon
• noNasals : MissingCommon
• noBilabialsOrNasals : MissingCommon
• noFricativesOrNasals : MissingCommon

instance Phenomena.Phonology.instDecidableEqMissingCommon : DecidableEq MissingCommon

Equations

• Phenomena.Phonology.instDecidableEqMissingCommon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqMissingCommon : BEq MissingCommon

Equations

• Phenomena.Phonology.instBEqMissingCommon = { beq := Phenomena.Phonology.instBEqMissingCommon.beq }

def Phenomena.Phonology.instBEqMissingCommon.beq : MissingCommon → MissingCommon → Bool

Equations

• Phenomena.Phonology.instBEqMissingCommon.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Phonology.instReprMissingCommon : Repr MissingCommon

Equations

• Phenomena.Phonology.instReprMissingCommon = { reprPrec := Phenomena.Phonology.instReprMissingCommon.repr }

def Phenomena.Phonology.instReprMissingCommon.repr : MissingCommon → Nat → Std.Format

Equations

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

inductive Phenomena.Phonology.UncommonPresent : Type

Presence of uncommon consonants (WALS Ch 19).

• none : UncommonPresent
• clicks : UncommonPresent
• labialVelars : UncommonPresent
• pharyngeals : UncommonPresent
• thSounds : UncommonPresent
• clicksPharyngealsAndTh : UncommonPresent
• pharyngealsAndTh : UncommonPresent

instance Phenomena.Phonology.instDecidableEqUncommonPresent : DecidableEq UncommonPresent

Equations

• Phenomena.Phonology.instDecidableEqUncommonPresent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Phonology.instBEqUncommonPresent : BEq UncommonPresent

Equations

• Phenomena.Phonology.instBEqUncommonPresent = { beq := Phenomena.Phonology.instBEqUncommonPresent.beq }

def Phenomena.Phonology.instBEqUncommonPresent.beq : UncommonPresent → UncommonPresent → Bool

Equations

• Phenomena.Phonology.instBEqUncommonPresent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Phonology.instReprUncommonPresent.repr : UncommonPresent → Nat → Std.Format

Equations

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

instance Phenomena.Phonology.instReprUncommonPresent : Repr UncommonPresent

Equations

• Phenomena.Phonology.instReprUncommonPresent = { reprPrec := Phenomena.Phonology.instReprUncommonPresent.repr }

structure Phenomena.Phonology.PhonProfile : Type

A language's phonological inventory and prosodic profile.

Combines 16 WALS features into a single record. Optional fields are used where a language may lack data for that chapter.

• cInventory : CInventorySize
• vInventory : VInventorySize
• cvRatio : CVRatio
• voicing : VoicingContrast
• uvulars : UvularPresence
• glottalized : GlottalizedType
• laterals : LateralType
• velarNasal : Option VelarNasalStatus
• nasalVowels : Option Bool
• frontRounded : FrontRounded
• syllables : SyllableComplexity
• tone : ToneSystem
• stress : Option StressLocation
• rhythm : Option RhythmType
• missingCommon : MissingCommon
• uncommon : UncommonPresent

instance Phenomena.Phonology.instDecidableEqPhonProfile : DecidableEq PhonProfile

Equations

• Phenomena.Phonology.instDecidableEqPhonProfile = Phenomena.Phonology.instDecidableEqPhonProfile.decEq

def Phenomena.Phonology.instDecidableEqPhonProfile.decEq (x✝ x✝¹ : PhonProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Phonology.instBEqPhonProfile.beq : PhonProfile → PhonProfile → Bool

Equations

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

instance Phenomena.Phonology.instBEqPhonProfile : BEq PhonProfile

Equations

• Phenomena.Phonology.instBEqPhonProfile = { beq := Phenomena.Phonology.instBEqPhonProfile.beq }

instance Phenomena.Phonology.instReprPhonProfile : Repr PhonProfile

Equations

• Phenomena.Phonology.instReprPhonProfile = { reprPrec := Phenomena.Phonology.instReprPhonProfile.repr }

def Phenomena.Phonology.instReprPhonProfile.repr : PhonProfile → Nat → Std.Format

Equations

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

def Phenomena.Phonology.english : PhonProfile

Equations

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

def Phenomena.Phonology.german : PhonProfile

Equations

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

def Phenomena.Phonology.finnish : PhonProfile

Equations

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

def Phenomena.Phonology.turkish : PhonProfile

Equations

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

def Phenomena.Phonology.russian : PhonProfile

Equations

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

def Phenomena.Phonology.french : PhonProfile

Equations

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

def Phenomena.Phonology.spanish : PhonProfile

Equations

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

def Phenomena.Phonology.japanese : PhonProfile

Equations

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

def Phenomena.Phonology.mandarin : PhonProfile

Equations

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

def Phenomena.Phonology.hindi : PhonProfile

Equations

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

def Phenomena.Phonology.georgian : PhonProfile

Equations

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

def Phenomena.Phonology.hungarian : PhonProfile

Equations

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

def Phenomena.Phonology.swahili : PhonProfile

Equations

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

def Phenomena.Phonology.yoruba : PhonProfile

Equations

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

def Phenomena.Phonology.maori : PhonProfile

Equations

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

def Phenomena.Phonology.zulu : PhonProfile

Equations

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

theorem Phenomena.Phonology.english_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "eng") = some english.cInventory

theorem Phenomena.Phonology.german_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "ger") = some german.cInventory

theorem Phenomena.Phonology.finnish_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "fin") = some finnish.cInventory

theorem Phenomena.Phonology.turkish_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "tur") = some turkish.cInventory

theorem Phenomena.Phonology.russian_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "rus") = some russian.cInventory

theorem Phenomena.Phonology.french_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "fre") = some french.cInventory

theorem Phenomena.Phonology.spanish_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "spa") = some spanish.cInventory

theorem Phenomena.Phonology.japanese_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "jpn") = some japanese.cInventory

theorem Phenomena.Phonology.mandarin_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "mnd") = some mandarin.cInventory

theorem Phenomena.Phonology.hindi_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "hin") = some hindi.cInventory

theorem Phenomena.Phonology.georgian_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "geo") = some georgian.cInventory

theorem Phenomena.Phonology.hungarian_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "hun") = some hungarian.cInventory

theorem Phenomena.Phonology.swahili_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "swa") = some swahili.cInventory

theorem Phenomena.Phonology.yoruba_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "yor") = some yoruba.cInventory

theorem Phenomena.Phonology.maori_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "mao") = some maori.cInventory

theorem Phenomena.Phonology.zulu_ch1 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => Phenomena.Phonology.fromWALS1A✝ x.value) (Core.WALS.F1A.lookup "zul") = some zulu.cInventory

theorem Phenomena.Phonology.english_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "eng") = some english.vInventory

theorem Phenomena.Phonology.german_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "ger") = some german.vInventory

theorem Phenomena.Phonology.finnish_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "fin") = some finnish.vInventory

theorem Phenomena.Phonology.turkish_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "tur") = some turkish.vInventory

theorem Phenomena.Phonology.russian_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "rus") = some russian.vInventory

theorem Phenomena.Phonology.french_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "fre") = some french.vInventory

theorem Phenomena.Phonology.spanish_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "spa") = some spanish.vInventory

theorem Phenomena.Phonology.japanese_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "jpn") = some japanese.vInventory

theorem Phenomena.Phonology.mandarin_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "mnd") = some mandarin.vInventory

theorem Phenomena.Phonology.hindi_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "hin") = some hindi.vInventory

theorem Phenomena.Phonology.georgian_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "geo") = some georgian.vInventory

theorem Phenomena.Phonology.hungarian_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "hun") = some hungarian.vInventory

theorem Phenomena.Phonology.swahili_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "swa") = some swahili.vInventory

theorem Phenomena.Phonology.yoruba_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "yor") = some yoruba.vInventory

theorem Phenomena.Phonology.maori_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "mao") = some maori.vInventory

theorem Phenomena.Phonology.zulu_ch2 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => Phenomena.Phonology.fromWALS2A✝ x.value) (Core.WALS.F2A.lookup "zul") = some zulu.vInventory

theorem Phenomena.Phonology.english_ch3 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F3A.ConsonantVowelRatio) => Phenomena.Phonology.fromWALS3A✝ x.value) (Core.WALS.F3A.lookup "eng") = some english.cvRatio

theorem Phenomena.Phonology.german_ch3 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F3A.ConsonantVowelRatio) => Phenomena.Phonology.fromWALS3A✝ x.value) (Core.WALS.F3A.lookup "ger") = some german.cvRatio

theorem Phenomena.Phonology.finnish_ch3 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F3A.ConsonantVowelRatio) => Phenomena.Phonology.fromWALS3A✝ x.value) (Core.WALS.F3A.lookup "fin") = some finnish.cvRatio

theorem Phenomena.Phonology.russian_ch3 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F3A.ConsonantVowelRatio) => Phenomena.Phonology.fromWALS3A✝ x.value) (Core.WALS.F3A.lookup "rus") = some russian.cvRatio

theorem Phenomena.Phonology.maori_ch3 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F3A.ConsonantVowelRatio) => Phenomena.Phonology.fromWALS3A✝ x.value) (Core.WALS.F3A.lookup "mao") = some maori.cvRatio

theorem Phenomena.Phonology.zulu_ch3 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F3A.ConsonantVowelRatio) => Phenomena.Phonology.fromWALS3A✝ x.value) (Core.WALS.F3A.lookup "zul") = some zulu.cvRatio

theorem Phenomena.Phonology.english_ch4 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F4A.VoicingInPlosivesAndFricatives) => Phenomena.Phonology.fromWALS4A✝ x.value) (Core.WALS.F4A.lookup "eng") = some english.voicing

theorem Phenomena.Phonology.german_ch4 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F4A.VoicingInPlosivesAndFricatives) => Phenomena.Phonology.fromWALS4A✝ x.value) (Core.WALS.F4A.lookup "ger") = some german.voicing

theorem Phenomena.Phonology.spanish_ch4 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F4A.VoicingInPlosivesAndFricatives) => Phenomena.Phonology.fromWALS4A✝ x.value) (Core.WALS.F4A.lookup "spa") = some spanish.voicing

theorem Phenomena.Phonology.mandarin_ch4 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F4A.VoicingInPlosivesAndFricatives) => Phenomena.Phonology.fromWALS4A✝ x.value) (Core.WALS.F4A.lookup "mnd") = some mandarin.voicing

theorem Phenomena.Phonology.maori_ch4 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F4A.VoicingInPlosivesAndFricatives) => Phenomena.Phonology.fromWALS4A✝ x.value) (Core.WALS.F4A.lookup "mao") = some maori.voicing

theorem Phenomena.Phonology.yoruba_ch4 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F4A.VoicingInPlosivesAndFricatives) => Phenomena.Phonology.fromWALS4A✝ x.value) (Core.WALS.F4A.lookup "yor") = some yoruba.voicing

theorem Phenomena.Phonology.english_ch6 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => Phenomena.Phonology.fromWALS6A✝ x.value) (Core.WALS.F6A.lookup "eng") = some english.uvulars

theorem Phenomena.Phonology.georgian_ch6 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => Phenomena.Phonology.fromWALS6A✝ x.value) (Core.WALS.F6A.lookup "geo") = some georgian.uvulars

theorem Phenomena.Phonology.french_ch6 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => Phenomena.Phonology.fromWALS6A✝ x.value) (Core.WALS.F6A.lookup "fre") = some french.uvulars

theorem Phenomena.Phonology.german_ch6 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => Phenomena.Phonology.fromWALS6A✝ x.value) (Core.WALS.F6A.lookup "ger") = some german.uvulars

theorem Phenomena.Phonology.english_ch7 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F7A.GlottalizedConsonants) => Phenomena.Phonology.fromWALS7A✝ x.value) (Core.WALS.F7A.lookup "eng") = some english.glottalized

theorem Phenomena.Phonology.georgian_ch7 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F7A.GlottalizedConsonants) => Phenomena.Phonology.fromWALS7A✝ x.value) (Core.WALS.F7A.lookup "geo") = some georgian.glottalized

theorem Phenomena.Phonology.zulu_ch7 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F7A.GlottalizedConsonants) => Phenomena.Phonology.fromWALS7A✝ x.value) (Core.WALS.F7A.lookup "zul") = some zulu.glottalized

theorem Phenomena.Phonology.english_ch8 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F8A.LateralConsonants) => Phenomena.Phonology.fromWALS8A✝ x.value) (Core.WALS.F8A.lookup "eng") = some english.laterals

theorem Phenomena.Phonology.japanese_ch8 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F8A.LateralConsonants) => Phenomena.Phonology.fromWALS8A✝ x.value) (Core.WALS.F8A.lookup "jpn") = some japanese.laterals

theorem Phenomena.Phonology.maori_ch8 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F8A.LateralConsonants) => Phenomena.Phonology.fromWALS8A✝ x.value) (Core.WALS.F8A.lookup "mao") = some maori.laterals

theorem Phenomena.Phonology.georgian_ch8 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F8A.LateralConsonants) => Phenomena.Phonology.fromWALS8A✝ x.value) (Core.WALS.F8A.lookup "geo") = some georgian.laterals

theorem Phenomena.Phonology.zulu_ch8 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F8A.LateralConsonants) => Phenomena.Phonology.fromWALS8A✝ x.value) (Core.WALS.F8A.lookup "zul") = some zulu.laterals

theorem Phenomena.Phonology.english_ch11 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F11A.FrontRoundedVowels) => Phenomena.Phonology.fromWALS11A✝ x.value) (Core.WALS.F11A.lookup "eng") = some english.frontRounded

theorem Phenomena.Phonology.finnish_ch11 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F11A.FrontRoundedVowels) => Phenomena.Phonology.fromWALS11A✝ x.value) (Core.WALS.F11A.lookup "fin") = some finnish.frontRounded

theorem Phenomena.Phonology.hungarian_ch11 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F11A.FrontRoundedVowels) => Phenomena.Phonology.fromWALS11A✝ x.value) (Core.WALS.F11A.lookup "hun") = some hungarian.frontRounded

theorem Phenomena.Phonology.french_ch11 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F11A.FrontRoundedVowels) => Phenomena.Phonology.fromWALS11A✝ x.value) (Core.WALS.F11A.lookup "fre") = some french.frontRounded

theorem Phenomena.Phonology.mandarin_ch11 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F11A.FrontRoundedVowels) => Phenomena.Phonology.fromWALS11A✝ x.value) (Core.WALS.F11A.lookup "mnd") = some mandarin.frontRounded

theorem Phenomena.Phonology.english_ch12 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => Phenomena.Phonology.fromWALS12A✝ x.value) (Core.WALS.F12A.lookup "eng") = some english.syllables

theorem Phenomena.Phonology.maori_ch12 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => Phenomena.Phonology.fromWALS12A✝ x.value) (Core.WALS.F12A.lookup "mao") = some maori.syllables

theorem Phenomena.Phonology.swahili_ch12 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => Phenomena.Phonology.fromWALS12A✝ x.value) (Core.WALS.F12A.lookup "swa") = some swahili.syllables

theorem Phenomena.Phonology.english_ch13 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => Phenomena.Phonology.fromWALS13A✝ x.value) (Core.WALS.F13A.lookup "eng") = some english.tone

theorem Phenomena.Phonology.mandarin_ch13 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => Phenomena.Phonology.fromWALS13A✝ x.value) (Core.WALS.F13A.lookup "mnd") = some mandarin.tone

theorem Phenomena.Phonology.yoruba_ch13 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => Phenomena.Phonology.fromWALS13A✝ x.value) (Core.WALS.F13A.lookup "yor") = some yoruba.tone

theorem Phenomena.Phonology.japanese_ch13 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => Phenomena.Phonology.fromWALS13A✝ x.value) (Core.WALS.F13A.lookup "jpn") = some japanese.tone

theorem Phenomena.Phonology.zulu_ch13 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => Phenomena.Phonology.fromWALS13A✝ x.value) (Core.WALS.F13A.lookup "zul") = some zulu.tone

theorem Phenomena.Phonology.english_ch14 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F14A.FixedStressLocations) => Phenomena.Phonology.fromWALS14A✝ x.value) (Core.WALS.F14A.lookup "eng") = some StressLocation.noFixed

theorem Phenomena.Phonology.finnish_ch14 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F14A.FixedStressLocations) => Phenomena.Phonology.fromWALS14A✝ x.value) (Core.WALS.F14A.lookup "fin") = some StressLocation.initial

theorem Phenomena.Phonology.hungarian_ch14 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F14A.FixedStressLocations) => Phenomena.Phonology.fromWALS14A✝ x.value) (Core.WALS.F14A.lookup "hun") = some StressLocation.initial

theorem Phenomena.Phonology.swahili_ch14 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F14A.FixedStressLocations) => Phenomena.Phonology.fromWALS14A✝ x.value) (Core.WALS.F14A.lookup "swa") = some StressLocation.penultimate

theorem Phenomena.Phonology.georgian_ch14 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F14A.FixedStressLocations) => Phenomena.Phonology.fromWALS14A✝ x.value) (Core.WALS.F14A.lookup "geo") = some StressLocation.antepenultimate

theorem Phenomena.Phonology.zulu_ch14 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F14A.FixedStressLocations) => Phenomena.Phonology.fromWALS14A✝ x.value) (Core.WALS.F14A.lookup "zul") = some StressLocation.penultimate

theorem Phenomena.Phonology.english_ch17 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F17A.RhythmTypes) => Phenomena.Phonology.fromWALS17A✝ x.value) (Core.WALS.F17A.lookup "eng") = some RhythmType.trochaic

theorem Phenomena.Phonology.turkish_ch17 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F17A.RhythmTypes) => Phenomena.Phonology.fromWALS17A✝ x.value) (Core.WALS.F17A.lookup "tur") = some RhythmType.noRhythm

theorem Phenomena.Phonology.russian_ch17 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F17A.RhythmTypes) => Phenomena.Phonology.fromWALS17A✝ x.value) (Core.WALS.F17A.lookup "rus") = some RhythmType.noRhythm

theorem Phenomena.Phonology.french_ch17 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F17A.RhythmTypes) => Phenomena.Phonology.fromWALS17A✝ x.value) (Core.WALS.F17A.lookup "fre") = some RhythmType.undetermined

theorem Phenomena.Phonology.english_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "eng") = some WeightStress.rightOriented

theorem Phenomena.Phonology.german_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "ger") = some WeightStress.rightOriented

theorem Phenomena.Phonology.finnish_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "fin") = some WeightStress.fixedNoWeight

theorem Phenomena.Phonology.turkish_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "tur") = some WeightStress.unbounded

theorem Phenomena.Phonology.russian_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "rus") = some WeightStress.unbounded

theorem Phenomena.Phonology.french_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "fre") = some WeightStress.rightEdge

theorem Phenomena.Phonology.spanish_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "spa") = some WeightStress.rightEdge

theorem Phenomena.Phonology.mandarin_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "mnd") = some WeightStress.notPredictable

theorem Phenomena.Phonology.hindi_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "hin") = some WeightStress.rightOriented

theorem Phenomena.Phonology.georgian_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "geo") = some WeightStress.fixedNoWeight

theorem Phenomena.Phonology.hungarian_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "hun") = some WeightStress.fixedNoWeight

theorem Phenomena.Phonology.swahili_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "swa") = some WeightStress.fixedNoWeight

theorem Phenomena.Phonology.maori_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "mao") = some WeightStress.unbounded

theorem Phenomena.Phonology.zulu_ch15 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => Phenomena.Phonology.fromWALS15A✝ x.value) (Core.WALS.F15A.lookup "zul") = some WeightStress.fixedNoWeight

theorem Phenomena.Phonology.english_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "eng") = some WeightFactor.longVowelOrCoda

theorem Phenomena.Phonology.german_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "ger") = some WeightFactor.codaConsonant

theorem Phenomena.Phonology.finnish_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "fin") = some WeightFactor.noWeight

theorem Phenomena.Phonology.turkish_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "tur") = some WeightFactor.lexicalStress

theorem Phenomena.Phonology.russian_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "rus") = some WeightFactor.lexicalStress

theorem Phenomena.Phonology.french_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "fre") = some WeightFactor.prominence

theorem Phenomena.Phonology.spanish_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "spa") = some WeightFactor.combined

theorem Phenomena.Phonology.mandarin_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "mnd") = some WeightFactor.lexicalStress

theorem Phenomena.Phonology.hindi_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "hin") = some WeightFactor.longVowelOrCoda

theorem Phenomena.Phonology.georgian_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "geo") = some WeightFactor.noWeight

theorem Phenomena.Phonology.hungarian_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "hun") = some WeightFactor.longVowel

theorem Phenomena.Phonology.swahili_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "swa") = some WeightFactor.noWeight

theorem Phenomena.Phonology.maori_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "mao") = some WeightFactor.longVowel

theorem Phenomena.Phonology.zulu_ch16 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => Phenomena.Phonology.fromWALS16A✝ x.value) (Core.WALS.F16A.lookup "zul") = some WeightFactor.noWeight

theorem Phenomena.Phonology.english_ch18 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F18A.AbsenceOfCommonConsonants) => Phenomena.Phonology.fromWALS18A✝ x.value) (Core.WALS.F18A.lookup "eng") = some english.missingCommon

theorem Phenomena.Phonology.english_ch19 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F19A.PresenceOfUncommonConsonants) => Phenomena.Phonology.fromWALS19A✝ x.value) (Core.WALS.F19A.lookup "eng") = some english.uncommon

theorem Phenomena.Phonology.spanish_ch19 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F19A.PresenceOfUncommonConsonants) => Phenomena.Phonology.fromWALS19A✝ x.value) (Core.WALS.F19A.lookup "spa") = some spanish.uncommon

theorem Phenomena.Phonology.zulu_ch19 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F19A.PresenceOfUncommonConsonants) => Phenomena.Phonology.fromWALS19A✝ x.value) (Core.WALS.F19A.lookup "zul") = some zulu.uncommon

theorem Phenomena.Phonology.yoruba_ch19 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F19A.PresenceOfUncommonConsonants) => Phenomena.Phonology.fromWALS19A✝ x.value) (Core.WALS.F19A.lookup "yor") = some yoruba.uncommon

theorem Phenomena.Phonology.ch1_average_modal : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => x.value == Core.WALS.F1A.ConsonantInventories.average) Phenomena.Phonology.ch1✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => x.value == Core.WALS.F1A.ConsonantInventories.small) Phenomena.Phonology.ch1✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => x.value == Core.WALS.F1A.ConsonantInventories.average) Phenomena.Phonology.ch1✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F1A.ConsonantInventories) => x.value == Core.WALS.F1A.ConsonantInventories.large) Phenomena.Phonology.ch1✝³).length

Ch 1: Average-sized consonant inventories are most common.

theorem Phenomena.Phonology.ch2_average_modal : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => x.value == Core.WALS.F2A.VowelQualityInventories.average) Phenomena.Phonology.ch2✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => x.value == Core.WALS.F2A.VowelQualityInventories.small) Phenomena.Phonology.ch2✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => x.value == Core.WALS.F2A.VowelQualityInventories.average) Phenomena.Phonology.ch2✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F2A.VowelQualityInventories) => x.value == Core.WALS.F2A.VowelQualityInventories.large) Phenomena.Phonology.ch2✝³).length

Ch 2: Average vowel inventories (5--6) are the majority.

theorem Phenomena.Phonology.ch6_no_uvulars_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => x.value == Core.WALS.F6A.UvularConsonants.none) Phenomena.Phonology.ch6✝).length > 4 * ((List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => x.value == Core.WALS.F6A.UvularConsonants.uvularStopsOnly) Phenomena.Phonology.ch6✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => x.value == Core.WALS.F6A.UvularConsonants.uvularContinuantsOnly) Phenomena.Phonology.ch6✝²).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F6A.UvularConsonants) => x.value == Core.WALS.F6A.UvularConsonants.uvularStopsAndContinuants) Phenomena.Phonology.ch6✝³).length)

Ch 6: The vast majority of languages lack uvular consonants.

theorem Phenomena.Phonology.ch7_no_glottalized_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F7A.GlottalizedConsonants) => x.value == Core.WALS.F7A.GlottalizedConsonants.noGlottalizedConsonants) Phenomena.Phonology.ch7✝).length > Phenomena.Phonology.ch7✝¹.length / 2

Ch 7: Most languages lack glottalized consonants.

theorem Phenomena.Phonology.ch12_moderate_modal : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => x.value == Core.WALS.F12A.SyllableStructure.moderatelyComplex) Phenomena.Phonology.ch12✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => x.value == Core.WALS.F12A.SyllableStructure.simple) Phenomena.Phonology.ch12✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => x.value == Core.WALS.F12A.SyllableStructure.moderatelyComplex) Phenomena.Phonology.ch12✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F12A.SyllableStructure) => x.value == Core.WALS.F12A.SyllableStructure.complex) Phenomena.Phonology.ch12✝³).length

Ch 12: Moderately complex syllable structure is most common.

theorem Phenomena.Phonology.ch13_no_tone_plurality : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => x.value == Core.WALS.F13A.Tone.noTones) Phenomena.Phonology.ch13✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => x.value == Core.WALS.F13A.Tone.simpleToneSystem) Phenomena.Phonology.ch13✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F13A.Tone) => x.value == Core.WALS.F13A.Tone.complexToneSystem) Phenomena.Phonology.ch13✝²).length

Ch 13: More languages lack tone than have it, but tonal languages are a substantial minority.

theorem Phenomena.Phonology.ch17_trochaic_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F17A.RhythmTypes) => x.value == Core.WALS.F17A.RhythmTypes.trochaic) Phenomena.Phonology.ch17✝).length > 4 * (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F17A.RhythmTypes) => x.value == Core.WALS.F17A.RhythmTypes.iambic) Phenomena.Phonology.ch17✝¹).length

Ch 17: Trochaic rhythm is overwhelmingly dominant among languages with rhythmic stress.

theorem Phenomena.Phonology.ch18_all_present_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F18A.AbsenceOfCommonConsonants) => x.value == Core.WALS.F18A.AbsenceOfCommonConsonants.allPresent) Phenomena.Phonology.ch18✝).length > Phenomena.Phonology.ch18✝¹.length * 8 / 10

Ch 18: The vast majority of languages have all common consonants (bilabials, fricatives, nasals).

theorem Phenomena.Phonology.ch10b_no_contrast_half : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F10B.NasalVowelsInWestAfrica) => x.value == Core.WALS.F10B.NasalVowelsInWestAfrica.noNasalVsOralVowelContrast) Phenomena.Phonology.ch10b✝).length = Phenomena.Phonology.ch10b✝¹.length / 2

Ch 10B: Half of the surveyed West African languages lack nasal vowel contrasts entirely.

theorem Phenomena.Phonology.ch15_fixed_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F15A.WeightSensitiveStress) => x.value == Core.WALS.F15A.WeightSensitiveStress.fixedStress) Phenomena.Phonology.ch15✝).length > Phenomena.Phonology.ch15✝¹.length / 2

Ch 15A: Fixed stress (no weight-sensitivity) is the majority pattern.

theorem Phenomena.Phonology.ch16_no_weight_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems) => x.value == Core.WALS.F16A.WeightFactorsInWeightSensitiveStressSystems.noWeight) Phenomena.Phonology.ch16✝).length > Phenomena.Phonology.ch16✝¹.length / 2

Ch 16A: More than half of languages show no syllable-weight effects on stress.

theorem Phenomena.Phonology.ch1_total : Phenomena.Phonology.ch1✝.length = 563

theorem Phenomena.Phonology.ch2_total : Phenomena.Phonology.ch2✝.length = 564

theorem Phenomena.Phonology.ch3_total : Phenomena.Phonology.ch3✝.length = 564

theorem Phenomena.Phonology.ch10b_total : Phenomena.Phonology.ch10b✝.length = 40

theorem Phenomena.Phonology.ch12_total : Phenomena.Phonology.ch12✝.length = 486

theorem Phenomena.Phonology.ch13_total : Phenomena.Phonology.ch13✝.length = 527

theorem Phenomena.Phonology.ch15_total : Phenomena.Phonology.ch15✝.length = 500

theorem Phenomena.Phonology.ch16_total : Phenomena.Phonology.ch16✝.length = 500