Cross-Linguistic Typology of Imperatives (WALS Chapters 70--73)

@cite{van-der-auwera-lejeune-2013}

Cross-linguistic data on imperative and related mood systems from four WALS chapters, all authored by Johan van der Auwera and Ludo @cite{van-der-auwera-lejeune-2013}.

Ch 70: The Morphological Imperative

Whether a language has a dedicated morphological form for second-person imperatives. Five values distinguishing number marking in the imperative paradigm: (1) second singular and second plural, (2) second singular only, (3) second plural only, (4) second person number-neutral, (5) no second-person imperatives.

Sample: 548 languages. The vast majority (426/548 = 77.7%) have a dedicated morphological imperative of some kind; only 122 lack one entirely.

Ch 71: The Prohibitive

How negative imperatives ("Don't!") are formed relative to regular imperatives and regular negation. Four structural types based on whether the imperative construction and the negation strategy are the same as in declaratives or special:

• Type 1: normal imperative + normal negation (e.g., Korean)
• Type 2: normal imperative + special negation (e.g., Ancient Greek)
• Type 3: special imperative + normal negation (e.g., Italian)
• Type 4: special imperative + special negation (e.g., Sinhala)

Sample: 496 languages. Type 2 (normal imperative + special negation) is the most common (182/496 = 36.7%).

Ch 72: Imperative-Hortative Systems

Whether the language has dedicated morphological forms for first-person hortatives ("let's go") and/or third-person jussives ("let him go"), in addition to the second-person imperative. Four values: imperative only, imperative + hortative, imperative + jussive, or all three.

Sample: 375 languages. Neither-type-of-system is the most common (201/375 = 53.6%); both-types-of-system is the least common (21/375 = 5.6%).

Ch 73: The Optative

Whether the language has a morphologically dedicated optative construction ("may it rain", "if only she were here"). Binary feature: present or absent.

Sample: 319 languages. Optatives are a minority feature: only 48/319 (15.0%) of sampled languages have a dedicated optative.

inductive Phenomena.Directives.Typology.MorphImpType : Type

WALS Ch 70: Whether a language has a dedicated morphological imperative.

Three categories based on the person distinctions available in the morphological imperative paradigm: (1) Second-person only: a dedicated imperative form exists only for 2nd person (singular and/or plural). (2) Second and other persons: the imperative paradigm extends beyond 2nd person to include 1st and/or 3rd person forms. (3) No morphological imperative: the language lacks a dedicated morphological imperative form; commands are expressed via bare stems, indicative forms, word order, particles, or intonation alone.

• secondOnly : MorphImpType

  Dedicated morphological imperative for second person only. (e.g., English Go!, Turkish Gel! 'Come!'). The most common pattern worldwide (426/548 = 77.7% have some morphological imperative; of those, second-person-only forms dominate).

• secondAndOther : MorphImpType

  Morphological imperative for second person and other persons (1st inclusive "let's", 3rd jussive, etc. are also morphologically imperative). (e.g., Latin i '2SG.IMP', eamus '1PL.IMP.SUBJ', Georgian, Quechua).

• noMorphological : MorphImpType

  No dedicated morphological imperative: commands use bare verb stems, indicative forms, particles, or intonation. (e.g., Mandarin Chinese, Thai, many isolating languages).

instance Phenomena.Directives.Typology.instDecidableEqMorphImpType : DecidableEq MorphImpType

Equations

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

def Phenomena.Directives.Typology.instBEqMorphImpType.beq : MorphImpType → MorphImpType → Bool

Equations

• Phenomena.Directives.Typology.instBEqMorphImpType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Directives.Typology.instBEqMorphImpType : BEq MorphImpType

Equations

• Phenomena.Directives.Typology.instBEqMorphImpType = { beq := Phenomena.Directives.Typology.instBEqMorphImpType.beq }

def Phenomena.Directives.Typology.instReprMorphImpType.repr : MorphImpType → Nat → Std.Format

Equations

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

instance Phenomena.Directives.Typology.instReprMorphImpType : Repr MorphImpType

Equations

• Phenomena.Directives.Typology.instReprMorphImpType = { reprPrec := Phenomena.Directives.Typology.instReprMorphImpType.repr }

inductive Phenomena.Directives.Typology.ProhibitiveType : Type

WALS Ch 71: How prohibitives (negative imperatives, "Don't!") are formed.

The classification cross-tabulates two binary features:

• Is the imperative construction the SAME as the affirmative imperative or SPECIAL (a different form)?
• Is the negation strategy the SAME as in declaratives or SPECIAL?

This yields four structural types. The key typological finding is that Type 1 (normal+normal) is surprisingly uncommon — languages tend to treat prohibitives differently from simple negation of an imperative.

• normalImpNormalNeg : ProhibitiveType

  Type 1: Normal imperative + normal negation. The prohibitive is simply the imperative plus regular sentential negation. (e.g., Korean ka-la 'go-IMP' → ka-ci mal-la 'go-NMLZ NEG-IMP'; Hungarian menj! → ne menj!).

• normalImpSpecialNeg : ProhibitiveType

  Type 2: Normal imperative + special negation. The imperative verb form is retained, but the negation marker is different from the one used in declaratives. (e.g., Ancient Greek: indicative ou vs imperative me; Tagalog: declarative hindi vs imperative huwag).

• specialImpNormalNeg : ProhibitiveType

  Type 3: Special imperative + normal negation. The negation strategy is the same as in declaratives, but the verb appears in a different form (e.g., subjunctive, infinitive, or a special negative imperative stem). (e.g., Italian va! IMP → non andare! NEG+INF; Finnish mene! IMP → ala mene NEG.AUX go.CONNEG).

• specialImpSpecialNeg : ProhibitiveType

  Type 4: Special imperative + special negation. Both the verb form and the negation marker differ from the declarative and the affirmative imperative. (e.g., Sinhala; many Austronesian and African languages).

instance Phenomena.Directives.Typology.instDecidableEqProhibitiveType : DecidableEq ProhibitiveType

Equations

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

def Phenomena.Directives.Typology.instBEqProhibitiveType.beq : ProhibitiveType → ProhibitiveType → Bool

Equations

• Phenomena.Directives.Typology.instBEqProhibitiveType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Directives.Typology.instBEqProhibitiveType : BEq ProhibitiveType

Equations

• Phenomena.Directives.Typology.instBEqProhibitiveType = { beq := Phenomena.Directives.Typology.instBEqProhibitiveType.beq }

instance Phenomena.Directives.Typology.instReprProhibitiveType : Repr ProhibitiveType

Equations

• Phenomena.Directives.Typology.instReprProhibitiveType = { reprPrec := Phenomena.Directives.Typology.instReprProhibitiveType.repr }

def Phenomena.Directives.Typology.instReprProhibitiveType.repr : ProhibitiveType → Nat → Std.Format

Equations

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

inductive Phenomena.Directives.Typology.ImpHortSystem : Type

WALS Ch 72: Whether the language has morphological hortative (1st person command: "let's go") and/or jussive (3rd person command: "let him go") in addition to the basic second-person imperative.

Four system types based on paradigm richness:

• Imperative only: only 2nd person morphological commands
• Imperative + hortative: 1st and 2nd person
• Imperative + jussive: 2nd and 3rd person
• All three: 1st, 2nd, and 3rd person

• imperativeOnly : ImpHortSystem

  Imperative only: the language has a morphological imperative (2nd person) but no dedicated hortative or jussive forms. (e.g., English Go! — "let's go" uses a periphrastic construction, not a morphological hortative).

• imperativeAndHortative : ImpHortSystem

  Imperative + hortative: the language has morphological forms for both 2nd person commands and 1st person (inclusive) hortatives ("let's"). (e.g., Turkish gel! 'come.IMP.2SG', gelelim 'come.HORT.1PL').

• imperativeAndJussive : ImpHortSystem

  Imperative + jussive: the language has morphological forms for both 2nd person commands and 3rd person jussives ("let him/them"). (e.g., Hindi-Urdu jao 'go.IMP.2PL', jaae 'go.JUSS.3SG').

• allThree : ImpHortSystem

  All three: the language has dedicated morphological forms for 2nd person imperatives, 1st person hortatives, and 3rd person jussives. (e.g., Latin i 'go.IMP.2SG', eamus 'go.SUBJ.1PL', eat 'go.SUBJ.3SG'; Georgian; Quechua).

instance Phenomena.Directives.Typology.instDecidableEqImpHortSystem : DecidableEq ImpHortSystem

Equations

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

instance Phenomena.Directives.Typology.instBEqImpHortSystem : BEq ImpHortSystem

Equations

• Phenomena.Directives.Typology.instBEqImpHortSystem = { beq := Phenomena.Directives.Typology.instBEqImpHortSystem.beq }

def Phenomena.Directives.Typology.instBEqImpHortSystem.beq : ImpHortSystem → ImpHortSystem → Bool

Equations

• Phenomena.Directives.Typology.instBEqImpHortSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Directives.Typology.instReprImpHortSystem : Repr ImpHortSystem

Equations

• Phenomena.Directives.Typology.instReprImpHortSystem = { reprPrec := Phenomena.Directives.Typology.instReprImpHortSystem.repr }

def Phenomena.Directives.Typology.instReprImpHortSystem.repr : ImpHortSystem → Nat → Std.Format

Equations

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

inductive Phenomena.Directives.Typology.OptativePresence : Type

WALS Ch 73: Whether the language has a morphologically dedicated optative.

An optative is a mood expressing wishes or hopes ("may it rain", "if only she were here", "long live the king"). The key criterion is whether the optative is morphologically distinct — languages that express wishes only via particles, intonation, or subjunctive forms shared with other functions are classified as lacking a dedicated optative.

• present : OptativePresence

  The language has a morphologically dedicated optative. (e.g., Ancient Greek -oimi / -oihn, Turkish -sA, Georgian, Finnish conditional used optatively).

• absent : OptativePresence

  The language lacks a dedicated morphological optative. Wishes are expressed by other means (subjunctive, particles, conditional, or periphrasis). (e.g., English, Mandarin Chinese, Japanese).

instance Phenomena.Directives.Typology.instDecidableEqOptativePresence : DecidableEq OptativePresence

Equations

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

def Phenomena.Directives.Typology.instBEqOptativePresence.beq : OptativePresence → OptativePresence → Bool

Equations

• Phenomena.Directives.Typology.instBEqOptativePresence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Directives.Typology.instBEqOptativePresence : BEq OptativePresence

Equations

• Phenomena.Directives.Typology.instBEqOptativePresence = { beq := Phenomena.Directives.Typology.instBEqOptativePresence.beq }

def Phenomena.Directives.Typology.instReprOptativePresence.repr : OptativePresence → Nat → Std.Format

Equations

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

instance Phenomena.Directives.Typology.instReprOptativePresence : Repr OptativePresence

Equations

• Phenomena.Directives.Typology.instReprOptativePresence = { reprPrec := Phenomena.Directives.Typology.instReprOptativePresence.repr }

structure Phenomena.Directives.Typology.WALSCount : Type

A single row in a WALS frequency table: a category label and its count.

• label : String
• count : Nat

def Phenomena.Directives.Typology.instReprWALSCount.repr : WALSCount → Nat → Std.Format

Equations

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

instance Phenomena.Directives.Typology.instReprWALSCount : Repr WALSCount

Equations

• Phenomena.Directives.Typology.instReprWALSCount = { reprPrec := Phenomena.Directives.Typology.instReprWALSCount.repr }

instance Phenomena.Directives.Typology.instDecidableEqWALSCount : DecidableEq WALSCount

Equations

• Phenomena.Directives.Typology.instDecidableEqWALSCount = Phenomena.Directives.Typology.instDecidableEqWALSCount.decEq

def Phenomena.Directives.Typology.instDecidableEqWALSCount.decEq (x✝ x✝¹ : WALSCount) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Directives.Typology.instBEqWALSCount.beq : WALSCount → WALSCount → Bool

Equations

• Phenomena.Directives.Typology.instBEqWALSCount.beq { label := a, count := a_1 } { label := b, count := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Directives.Typology.instBEqWALSCount.beq x✝¹ x✝ = false

instance Phenomena.Directives.Typology.instBEqWALSCount : BEq WALSCount

Equations

• Phenomena.Directives.Typology.instBEqWALSCount = { beq := Phenomena.Directives.Typology.instBEqWALSCount.beq }

def Phenomena.Directives.Typology.WALSCount.totalOf (cs : List WALSCount) : Nat

Sum of counts in a WALS table.

Equations

• Phenomena.Directives.Typology.WALSCount.totalOf cs = List.foldl (fun (acc : Nat) (c : Phenomena.Directives.Typology.WALSCount) => acc + c.count) 0 cs

def Phenomena.Directives.Typology.ch70Counts : List WALSCount

Chapter 70 distribution: morphological imperative types (N = 548).

Equations

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

def Phenomena.Directives.Typology.ch71Counts : List WALSCount

Chapter 71 distribution: prohibitive types (N = 496).

Equations

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

def Phenomena.Directives.Typology.ch72Counts : List WALSCount

Chapter 72 distribution: imperative-hortative systems (N = 375).

Equations

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

def Phenomena.Directives.Typology.ch73Counts : List WALSCount

Chapter 73 distribution: optative presence (N = 319).

Equations

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

theorem Phenomena.Directives.Typology.ch70_total : WALSCount.totalOf ch70Counts = 548

Ch 70 total: 548 languages.

theorem Phenomena.Directives.Typology.ch71_total : WALSCount.totalOf ch71Counts = 496

Ch 71 total: 496 languages.

theorem Phenomena.Directives.Typology.ch72_total : WALSCount.totalOf ch72Counts = 375

Ch 72 total: 375 languages.

theorem Phenomena.Directives.Typology.ch73_total : WALSCount.totalOf ch73Counts = 319

Ch 73 total: 319 languages.

structure Phenomena.Directives.Typology.ImperativeProfile : Type

A language's imperative system profile across WALS Chapters 70--73.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• morphImp : MorphImpType

  Ch 70: Morphological imperative type.

• prohibitive : ProhibitiveType

  Ch 71: Prohibitive construction type.

• impHortSystem : ImpHortSystem

  Ch 72: Imperative-hortative system.

• optative : Option OptativePresence

  Ch 73: Optative presence (none if language not in Ch 73 sample).

• impForms : List String

  Illustrative imperative form(s).

• notes : String

  Notes on the imperative system.

def Phenomena.Directives.Typology.instReprImperativeProfile.repr : ImperativeProfile → Nat → Std.Format

Equations

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

instance Phenomena.Directives.Typology.instReprImperativeProfile : Repr ImperativeProfile

Equations

• Phenomena.Directives.Typology.instReprImperativeProfile = { reprPrec := Phenomena.Directives.Typology.instReprImperativeProfile.repr }

def Phenomena.Directives.Typology.english : ImperativeProfile

English: second-person-only morphological imperative (Go!, Be quiet!). The imperative is typically the bare stem, identical to the infinitive but distinguished from declaratives by the absence of a subject and do-support. Prohibitives use the regular negation strategy with do-support: Don't go! — normal imperative with normal negation (Type 1). No dedicated hortative (*Go-we!); periphrastic Let's go instead. No morphological optative; wishes expressed by may or subjunctive relics (Long live the king).

Equations

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

def Phenomena.Directives.Typology.japanese : ImperativeProfile

Japanese: second-person-only morphological imperative. The plain imperative suffix -e / -ro is used for 2nd person commands (ike! 'go!', tabero! 'eat!'). Prohibitives use the negative form -na which is a special negation marker distinct from the declarative -nai: iku-na! 'go-PROH' — normal imperative stem + special negation (Type 2). No dedicated hortative morphology; volitional -ou / -you serves a related but distinct function. No morphological optative.

Equations

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

def Phenomena.Directives.Typology.mandarin : ImperativeProfile

Mandarin Chinese: no morphological imperative. Commands are expressed by bare verb forms, intonation, and sentence-final particles (ba, a). Zou! 'Go!' is identical to the declarative verb form. Prohibitives use the special negative particle bie (别) rather than the declarative bu or mei: bie zou! 'PROH go' — no morphological imperative + special negation (closest to Type 2, but no morphological imperative at all). No hortative or jussive morphology. No optative.

Equations

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

def Phenomena.Directives.Typology.turkish : ImperativeProfile

Turkish: second-person and other-person morphological imperative. Turkish has a full imperative paradigm: 2SG gel (bare stem), 2PL gelin, 3SG gelsin, 3PL gelsinler, and 1PL hortative gelelim. Prohibitives use the regular negative suffix -mA- with the imperative: gelme! 'come-NEG.IMP' — normal imperative + normal negation (Type 1). Has both hortative and jussive morphology (all three). Optative expressed by the suffix -sA (desiderative/conditional).

Equations

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

def Phenomena.Directives.Typology.finnish : ImperativeProfile

Finnish: second-person morphological imperative with dedicated forms (mene! 'go.IMP.2SG', menkaa! 'go.IMP.2PL'). Prohibitives use the negative auxiliary verb ala (imperative form of the negative verb ei) followed by the connegative: ala mene! 'NEG.IMP go.CONNEG' — the verb form changes from imperative to connegative (special imperative + normal negation, Type 3). Has hortative and jussive morphology. No dedicated optative (conditional -isi- serves optative functions).

Equations

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

def Phenomena.Directives.Typology.russian : ImperativeProfile

Russian: second-person-only morphological imperative (idi! 'go.IMP.2SG', idite! 'go.IMP.2PL'). Prohibitives use the regular negation ne with the imperative form: ne idi! 'NEG go.IMP' — normal imperative + normal negation (Type 1). Periphrastic hortative davaj(te) + infinitive/verb. No dedicated optative morphology.

Equations

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

def Phenomena.Directives.Typology.latin : ImperativeProfile

Latin: full morphological imperative paradigm with forms for 2SG, 2PL, and future imperative. Also has subjunctive forms used as hortative (1PL) and jussive (3SG/3PL): i! 'go.IMP.2SG', ite! 'go.IMP.2PL', eamus! 'go.SUBJ.1PL' (hortative), eat! 'go.SUBJ.3SG' (jussive). Prohibitives use the special negative ne (distinct from declarative non) with the subjunctive: ne eas! 'PROH go.SUBJ.2SG' — special imperative form (subjunctive replaces imperative) + special negation (Type 4). No dedicated optative (wishes use subjunctive).

Equations

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

def Phenomena.Directives.Typology.hindiUrdu : ImperativeProfile

Hindi-Urdu: second-person and other-person morphological imperative. Three levels of imperative politeness: intimate (ja 'go.IMP.2SG.INTIM'), familiar (jao 'go.IMP.2PL'), and polite (jaiye 'go.IMP.2HON'). 3SG jussive jaae. Prohibitives use mat (special negative particle distinct from declarative nahin): mat jao! 'PROH go' — normal imperative + special negation (Type 2). No dedicated optative.

Equations

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

def Phenomena.Directives.Typology.swahili : ImperativeProfile

Swahili: second-person and other-person morphological imperative. 2SG imperative is the bare stem (njoo! 'come!', soma! 'read!'); 2PL adds -ni (njooni!). Subjunctive forms serve as hortative/jussive: tu-some '1PL-read.SUBJ' (hortative), a-some '3SG-read.SUBJ' (jussive). Prohibitives use the regular negative prefix usi- with subjunctive: usi-some! 'NEG.2SG-read.SUBJ' — special verb form + normal negation strategy (Type 3). No dedicated optative.

Equations

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

def Phenomena.Directives.Typology.arabic : ImperativeProfile

Arabic (Modern Standard): second-person and other-person morphological imperative. 2SG.M uktub! 'write!', 2SG.F uktubii!. Jussive (3rd person) uses the jussive mood li-yaktub 'let him write'. Prohibitives use the special negative particle laa (distinct from declarative lam/lan/maa) with the jussive verb form: laa taktub! 'PROH write.JUSS' — special verb form + special negation (Type 4). No dedicated optative.

Equations

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

def Phenomena.Directives.Typology.tagalog : ImperativeProfile

Tagalog: no morphological imperative in the strict sense; commands use the basic verb form (infinitive/imperative neutral form). Prohibitives use the special negative huwag (distinct from declarative hindi): Huwag kang pumunta! 'PROH you go' — normal imperative + special negation (Type 2). Periphrastic hortative with tayo na 'us already'. No optative.

Equations

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

def Phenomena.Directives.Typology.quechua : ImperativeProfile

Quechua (Cuzco): second-person and other-person morphological imperative with a rich paradigm. 2SG -y (ri-y! 'go-IMP.2SG'), 2PL -ychis. 1PL hortative -sun (ri-sun 'go-HORT.1PL'), 3SG jussive -chun (ri-chun 'go-JUSS.3SG'). Prohibitives use the regular negation ama with the imperative followed by the suffix -chu: ama ri-y-chu! 'PROH go-IMP-PROH' — this involves a special construction (special imperative + special negation, Type 4, since both ama and -chu are prohibitive-specific). Has a dedicated optative (desiderative) suffix.

Equations

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

def Phenomena.Directives.Typology.georgian : ImperativeProfile

Georgian: second-person and other-person morphological imperative. Georgian has a complex verbal system with imperative, optative, and conjunctive moods. 2SG ts'eri! 'write!'. Prohibitives use the preverb nu- and the conjunctive: nu ts'er — special verb form + special construction (Type 4). Has all three: imperative, hortative (1PL), and jussive (3SG). Morphologically dedicated optative mood exists.

Equations

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

def Phenomena.Directives.Typology.hungarian : ImperativeProfile

Hungarian: second-person-only morphological imperative. 2SG menj! 'go!', 2PL menjetek!. Prohibitives use the regular negation ne with the imperative/subjunctive form: ne menj! 'NEG go.IMP' — normal imperative + normal negation (Type 1). Subjunctive serves as jussive for 3rd person. No dedicated optative.

Equations

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

def Phenomena.Directives.Typology.korean : ImperativeProfile

Korean: second-person morphological imperative with speech-level distinctions. Imperative endings vary by politeness: -a/eo (plain), -seyo (polite), -(eu)sipsiyo (formal). Prohibitives use regular negation -ji ma- with the imperative: ga-ji ma! 'go-NMLZ NEG.IMP' — the structure involves the same imperative construction and the verbal negation pattern with mal- (normal imperative + normal negation, Type 1). Hortative -ja for 1PL. No dedicated optative.

Equations

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

def Phenomena.Directives.Typology.italian : ImperativeProfile

Italian: second-person morphological imperative. 2SG va'! 'go!', 2PL andate!. Prohibitives use the regular negation non but with the infinitive instead of the imperative for 2SG: Non andare! 'NEG go.INF' — special verb form (infinitive replaces imperative) + normal negation (Type 3). 3SG/3PL uses subjunctive as jussive. No dedicated optative (subjunctive covers wishes).

Equations

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

def Phenomena.Directives.Typology.ancientGreek : ImperativeProfile

Ancient Greek: second-person and other-person morphological imperative with present and aorist stems. Prohibitives use the special negative me (distinct from declarative ou/ouk) with the subjunctive (aorist) or imperative (present): me graphe! 'PROH write' — normal imperative form

• special negation (Type 2 for present imperative prohibitives). Rich optative mood paradigm (graphoimi 'may I write').

Equations

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

def Phenomena.Directives.Typology.allLanguages : List ImperativeProfile

All language profiles in the sample.

Equations

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

def Phenomena.Directives.Typology.ImperativeProfile.hasMorphImp (p : ImperativeProfile) : Bool

Does a language have a morphological imperative (of any type)?

Equations

• p.hasMorphImp = (p.morphImp != Phenomena.Directives.Typology.MorphImpType.noMorphological)

def Phenomena.Directives.Typology.ImperativeProfile.hasExtendedParadigm (p : ImperativeProfile) : Bool

Does a language have an extended imperative paradigm (beyond 2nd person)?

Equations

• p.hasExtendedParadigm = (p.morphImp == Phenomena.Directives.Typology.MorphImpType.secondAndOther)

def Phenomena.Directives.Typology.ImperativeProfile.hasHortative (p : ImperativeProfile) : Bool

Does a language have a hortative (either with or without jussive)?

Equations

• p.hasHortative = (p.impHortSystem == Phenomena.Directives.Typology.ImpHortSystem.imperativeAndHortative || p.impHortSystem == Phenomena.Directives.Typology.ImpHortSystem.allThree)

def Phenomena.Directives.Typology.ImperativeProfile.hasJussive (p : ImperativeProfile) : Bool

Does a language have a jussive (either with or without hortative)?

Equations

• p.hasJussive = (p.impHortSystem == Phenomena.Directives.Typology.ImpHortSystem.imperativeAndJussive || p.impHortSystem == Phenomena.Directives.Typology.ImpHortSystem.allThree)

def Phenomena.Directives.Typology.ImperativeProfile.hasOptative (p : ImperativeProfile) : Bool

Does a language have a dedicated optative?

Equations

• p.hasOptative = (p.optative == some Phenomena.Directives.Typology.OptativePresence.present)

def Phenomena.Directives.Typology.ImperativeProfile.hasSpecialProhibitive (p : ImperativeProfile) : Bool

Does a language use a special prohibitive construction (Type 2, 3, or 4)? That is, does the prohibitive differ from simply negating the imperative?

Equations

• p.hasSpecialProhibitive = (p.prohibitive != Phenomena.Directives.Typology.ProhibitiveType.normalImpNormalNeg)

def Phenomena.Directives.Typology.countByMorphImp (langs : List ImperativeProfile) (t : MorphImpType) : Nat

Count of languages with a given morphological imperative type.

Equations

• Phenomena.Directives.Typology.countByMorphImp langs t = (List.filter (fun (x : Phenomena.Directives.Typology.ImperativeProfile) => x.morphImp == t) langs).length

def Phenomena.Directives.Typology.countByProhibitive (langs : List ImperativeProfile) (t : ProhibitiveType) : Nat

Count of languages with a given prohibitive type.

Equations

• Phenomena.Directives.Typology.countByProhibitive langs t = (List.filter (fun (x : Phenomena.Directives.Typology.ImperativeProfile) => x.prohibitive == t) langs).length

def Phenomena.Directives.Typology.countByImpHort (langs : List ImperativeProfile) (t : ImpHortSystem) : Nat

Count of languages with a given imperative-hortative system.

Equations

• Phenomena.Directives.Typology.countByImpHort langs t = (List.filter (fun (x : Phenomena.Directives.Typology.ImperativeProfile) => x.impHortSystem == t) langs).length

theorem Phenomena.Directives.Typology.morph_imp_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value != Core.WALS.F70A.MorphologicalImperative.noSecondPersonImperatives) Phenomena.Directives.Typology.f70✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.noSecondPersonImperatives) Phenomena.Directives.Typology.f70✝¹).length * 3

Ch 70: Languages with a morphological imperative (426/548 = 77.7%) vastly outnumber those without (122/548 = 22.3%).

theorem Phenomena.Directives.Typology.sg_pl_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondSingularAndSecondPlural) Phenomena.Directives.Typology.f70✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondPersonNumberNeutral) Phenomena.Directives.Typology.f70✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondSingularAndSecondPlural) Phenomena.Directives.Typology.f70✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.noSecondPersonImperatives) Phenomena.Directives.Typology.f70✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondSingularAndSecondPlural) Phenomena.Directives.Typology.f70✝⁴).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondSingular) Phenomena.Directives.Typology.f70✝⁵).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondSingularAndSecondPlural) Phenomena.Directives.Typology.f70✝⁶).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => x.value == Core.WALS.F70A.MorphologicalImperative.secondPlural) Phenomena.Directives.Typology.f70✝⁷).length

Ch 70: Second-singular-and-second-plural imperatives (292) are the most common single type.

theorem Phenomena.Directives.Typology.prohibitive_mostly_special : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value != Core.WALS.F71A.Prohibitive.normalImperativeNormalNegative) Phenomena.Directives.Typology.f71✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.normalImperativeNormalNegative) Phenomena.Directives.Typology.f71✝¹).length * 3

Ch 71: The majority of languages (383/496 = 77.2%) use a special construction for prohibitives — they do NOT simply negate the imperative. Only 113/496 (22.8%) use normal imperative + normal negation (Type 1). This is van der Auwera's key finding: prohibitives are typologically marked relative to affirmative imperatives.

theorem Phenomena.Directives.Typology.type2_most_common_prohibitive : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.normalImperativeSpecialNegative) Phenomena.Directives.Typology.f71✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.specialImperativeSpecialNegative) Phenomena.Directives.Typology.f71✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.specialImperativeSpecialNegative) Phenomena.Directives.Typology.f71✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.normalImperativeNormalNegative) Phenomena.Directives.Typology.f71✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.normalImperativeNormalNegative) Phenomena.Directives.Typology.f71✝⁴).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => x.value == Core.WALS.F71A.Prohibitive.specialImperativeNormalNegative) Phenomena.Directives.Typology.f71✝⁵).length

Ch 71: Type 2 (normal imperative + special negation) is the single most common prohibitive type: 182 > 146 > 113 > 55.

theorem Phenomena.Directives.Typology.neither_system_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.neitherTypeOfSystem) Phenomena.Directives.Typology.f72✝).length > Phenomena.Directives.Typology.f72✝¹.length / 2

Ch 72: More than half of languages (201/375 = 53.6%) have neither type of imperative-hortative system.

theorem Phenomena.Directives.Typology.minimal_system_rarest : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.minimalSystem) Phenomena.Directives.Typology.f72✝).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.bothTypesOfSystem) Phenomena.Directives.Typology.f72✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.minimalSystem) Phenomena.Directives.Typology.f72✝²).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.maximalSystem) Phenomena.Directives.Typology.f72✝³).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.minimalSystem) Phenomena.Directives.Typology.f72✝⁴).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.neitherTypeOfSystem) Phenomena.Directives.Typology.f72✝⁵).length

Ch 72: Minimal systems (20/375 = 5.3%) are the rarest type.

theorem Phenomena.Directives.Typology.maximal_more_common_than_minimal : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.maximalSystem) Phenomena.Directives.Typology.f72✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.minimalSystem) Phenomena.Directives.Typology.f72✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => x.value == Core.WALS.F72A.ImperativeHortativeSystems.bothTypesOfSystem) Phenomena.Directives.Typology.f72✝²).length

Ch 72: Maximal systems (133) are much more common than minimal systems (20) or both-types systems (21).

theorem Phenomena.Directives.Typology.optative_minority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => x.value == Core.WALS.F73A.Optative.inflectionalOptativeAbsent) Phenomena.Directives.Typology.f73✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => x.value == Core.WALS.F73A.Optative.inflectionalOptativePresent) Phenomena.Directives.Typology.f73✝¹).length * 5

Ch 73: The majority of languages lack a dedicated optative (271/319). Only 48/319 (15.0%) have one. Optatives outnumbered by non-optatives more than 5:1.

theorem Phenomena.Directives.Typology.all_three_implies_extended_paradigm : have allThreeLangs := List.filter (fun (x : ImperativeProfile) => x.impHortSystem == ImpHortSystem.allThree) allLanguages; (allThreeLangs.all fun (x : ImperativeProfile) => x.hasExtendedParadigm) = true

In our sample, every language with an "all three" imperative-hortative system (Ch 72) also has a second-and-other morphological imperative (Ch 70). This makes sense: if a language has morphological hortative and jussive forms, its imperative paradigm extends beyond 2nd person.

theorem Phenomena.Directives.Typology.sample_special_prohibitive_majority : have special := List.filter (fun (x : ImperativeProfile) => x.hasSpecialProhibitive) allLanguages; have normal := List.filter (fun (x : ImperativeProfile) => decide ¬x.hasSpecialProhibitive = true) allLanguages; special.length > normal.length

In our sample, more languages have a special prohibitive construction (Type 2, 3, or 4) than a normal one (Type 1). This mirrors the WALS finding that simply negating the imperative is the exception, not the rule.

theorem Phenomena.Directives.Typology.optative_implies_extended_paradigm : have optLangs := List.filter (fun (x : ImperativeProfile) => x.hasOptative) allLanguages; (optLangs.all fun (x : ImperativeProfile) => x.hasExtendedParadigm) = true

In our sample, every language with a dedicated optative also has a second-and-other morphological imperative (extended paradigm). Rich mood morphology tends to come as a package.

theorem Phenomena.Directives.Typology.no_morph_imp_implies_imp_only : have noMorph := List.filter (fun (x : ImperativeProfile) => x.morphImp == MorphImpType.noMorphological) allLanguages; (noMorph.all fun (x : ImperativeProfile) => x.impHortSystem == ImpHortSystem.imperativeOnly) = true

In our sample, languages without a morphological imperative (Ch 70) are always classified as imperative-only for Ch 72. This is expected: if a language lacks even a 2nd-person morphological imperative, it is unlikely to have morphological hortatives or jussives.

theorem Phenomena.Directives.Typology.jussive_mostly_extended_paradigm : have jussLangs := List.filter (fun (x : ImperativeProfile) => x.hasJussive) allLanguages; have extended := List.filter (fun (x : ImperativeProfile) => x.hasExtendedParadigm) jussLangs; extended.length * 4 ≥ jussLangs.length * 3

In our sample, most languages with a jussive (Ch 72) also have a second-and-other morphological imperative (Ch 70). The exception is Hungarian, where the subjunctive serves as jussive while the imperative paradigm is second-person-only. At least 3/4 of jussive languages have extended paradigms.

theorem Phenomena.Directives.Typology.type1_languages : have type1 := List.filter (fun (x : ImperativeProfile) => x.prohibitive == ProhibitiveType.normalImpNormalNeg) allLanguages; type1.length = 5

In our sample, Turkish, Russian, Hungarian, English, and Korean all use Type 1 prohibitives (normal imperative + normal negation). These include agglutinative languages where negation is a regular affix/particle that combines freely with the imperative morphology.

theorem Phenomena.Directives.Typology.english_second_only : (english.morphImp == MorphImpType.secondOnly) = true

theorem Phenomena.Directives.Typology.japanese_second_only : (japanese.morphImp == MorphImpType.secondOnly) = true

theorem Phenomena.Directives.Typology.mandarin_no_morph : (mandarin.morphImp == MorphImpType.noMorphological) = true

theorem Phenomena.Directives.Typology.turkish_extended : turkish.hasExtendedParadigm = true

theorem Phenomena.Directives.Typology.finnish_extended : finnish.hasExtendedParadigm = true

theorem Phenomena.Directives.Typology.latin_extended : latin.hasExtendedParadigm = true

theorem Phenomena.Directives.Typology.tagalog_no_morph : (tagalog.morphImp == MorphImpType.noMorphological) = true

theorem Phenomena.Directives.Typology.english_type1 : (english.prohibitive == ProhibitiveType.normalImpNormalNeg) = true

theorem Phenomena.Directives.Typology.japanese_type2 : (japanese.prohibitive == ProhibitiveType.normalImpSpecialNeg) = true

theorem Phenomena.Directives.Typology.finnish_type3 : (finnish.prohibitive == ProhibitiveType.specialImpNormalNeg) = true

theorem Phenomena.Directives.Typology.latin_type4 : (latin.prohibitive == ProhibitiveType.specialImpSpecialNeg) = true

theorem Phenomena.Directives.Typology.italian_type3 : (italian.prohibitive == ProhibitiveType.specialImpNormalNeg) = true

theorem Phenomena.Directives.Typology.arabic_type4 : (arabic.prohibitive == ProhibitiveType.specialImpSpecialNeg) = true

theorem Phenomena.Directives.Typology.hindiUrdu_type2 : (hindiUrdu.prohibitive == ProhibitiveType.normalImpSpecialNeg) = true

theorem Phenomena.Directives.Typology.english_imp_only : (english.impHortSystem == ImpHortSystem.imperativeOnly) = true

theorem Phenomena.Directives.Typology.turkish_all_three : (turkish.impHortSystem == ImpHortSystem.allThree) = true

theorem Phenomena.Directives.Typology.korean_imp_hort : (korean.impHortSystem == ImpHortSystem.imperativeAndHortative) = true

theorem Phenomena.Directives.Typology.hungarian_imp_juss : (hungarian.impHortSystem == ImpHortSystem.imperativeAndJussive) = true

theorem Phenomena.Directives.Typology.quechua_all_three : (quechua.impHortSystem == ImpHortSystem.allThree) = true

theorem Phenomena.Directives.Typology.georgian_all_three : (georgian.impHortSystem == ImpHortSystem.allThree) = true

theorem Phenomena.Directives.Typology.turkish_has_optative : turkish.hasOptative = true

theorem Phenomena.Directives.Typology.english_no_optative : (english.optative == some OptativePresence.absent) = true

theorem Phenomena.Directives.Typology.greek_has_optative : ancientGreek.hasOptative = true

theorem Phenomena.Directives.Typology.quechua_has_optative : quechua.hasOptative = true

theorem Phenomena.Directives.Typology.georgian_has_optative : georgian.hasOptative = true

theorem Phenomena.Directives.Typology.extended_implies_beyond_imp_only : have extended := List.filter (fun (x : ImperativeProfile) => x.hasExtendedParadigm) allLanguages; (extended.all fun (x : ImperativeProfile) => x.impHortSystem != ImpHortSystem.imperativeOnly) = true

In our sample, every language with a morphological imperative that extends to other persons (Ch 70 = secondAndOther) has at least some non-second-person command morphology (Ch 72 ≠ imperativeOnly), unless the extension is limited to features like number or formality within 2nd person. In fact, all secondAndOther languages in our sample have hortative or jussive or both.

theorem Phenomena.Directives.Typology.no_morph_imp_no_optative : have noMorph := List.filter (fun (x : ImperativeProfile) => x.morphImp == MorphImpType.noMorphological) allLanguages; (noMorph.all fun (x : ImperativeProfile) => decide ¬x.hasOptative = true) = true

In our sample, no language without a morphological imperative has a dedicated optative. Mood-poor languages tend to be consistently mood-poor across the board.

theorem Phenomena.Directives.Typology.optative_mostly_special_prohibitive : have optLangs := List.filter (fun (x : ImperativeProfile) => x.hasOptative) allLanguages; have special := List.filter (fun (x : ImperativeProfile) => x.hasSpecialProhibitive) optLangs; special.length * 4 ≥ optLangs.length * 3

In our sample, most languages with a dedicated optative also have a special prohibitive construction (Type 2, 3, or 4). The exception is Turkish, where both the optative (-sA) and the prohibitive (regular negation + imperative) are well-integrated into the agglutinative morphology. At least 3/4 of optative languages have special prohibitives.

theorem Phenomena.Directives.Typology.ch_sample_sizes : WALSCount.totalOf ch70Counts = 548 ∧ WALSCount.totalOf ch71Counts = 496 ∧ WALSCount.totalOf ch72Counts = 375 ∧ WALSCount.totalOf ch73Counts = 319

Chapters 70--73 have different sample sizes.

theorem Phenomena.Directives.Typology.sample_size : allLanguages.length = 17

Number of languages in our sample.

theorem Phenomena.Directives.Typology.sample_second_only_count : countByMorphImp allLanguages MorphImpType.secondOnly = 6

Morphological imperative distribution in our sample.

theorem Phenomena.Directives.Typology.sample_second_and_other_count : countByMorphImp allLanguages MorphImpType.secondAndOther = 9

theorem Phenomena.Directives.Typology.sample_no_morph_count : countByMorphImp allLanguages MorphImpType.noMorphological = 2

theorem Phenomena.Directives.Typology.sample_type1_count : countByProhibitive allLanguages ProhibitiveType.normalImpNormalNeg = 5

Prohibitive type distribution in our sample.

theorem Phenomena.Directives.Typology.sample_type2_count : countByProhibitive allLanguages ProhibitiveType.normalImpSpecialNeg = 5

theorem Phenomena.Directives.Typology.sample_type3_count : countByProhibitive allLanguages ProhibitiveType.specialImpNormalNeg = 3

theorem Phenomena.Directives.Typology.sample_type4_count : countByProhibitive allLanguages ProhibitiveType.specialImpSpecialNeg = 4

theorem Phenomena.Directives.Typology.sample_imp_only_count : countByImpHort allLanguages ImpHortSystem.imperativeOnly = 5

Imperative-hortative system distribution in our sample.

theorem Phenomena.Directives.Typology.sample_imp_hort_count : countByImpHort allLanguages ImpHortSystem.imperativeAndHortative = 1

theorem Phenomena.Directives.Typology.sample_imp_juss_count : countByImpHort allLanguages ImpHortSystem.imperativeAndJussive = 4

theorem Phenomena.Directives.Typology.sample_all_three_count : countByImpHort allLanguages ImpHortSystem.allThree = 7

theorem Phenomena.Directives.Typology.sample_optative_present_count : (List.filter (fun (x : ImperativeProfile) => x.hasOptative) allLanguages).length = 4

Optative distribution in our sample.

theorem Phenomena.Directives.Typology.sample_optative_absent_count : (List.filter (fun (x : ImperativeProfile) => x.optative == some OptativePresence.absent) allLanguages).length = 13

theorem Phenomena.Directives.Typology.sample_all_have_optative_data : (allLanguages.all fun (x : ImperativeProfile) => x.optative != none) = true

Every language in our sample has a Ch 73 classification.

theorem Phenomena.Directives.Typology.ch70_wals_total : Phenomena.Directives.Typology.f70✝.length = 548

theorem Phenomena.Directives.Typology.ch71_wals_total : Phenomena.Directives.Typology.f71✝.length = 496

theorem Phenomena.Directives.Typology.ch72_wals_total : Phenomena.Directives.Typology.f72✝.length = 375

theorem Phenomena.Directives.Typology.ch73_wals_total : Phenomena.Directives.Typology.f73✝.length = 319

theorem Phenomena.Directives.Typology.mandarin_ch70 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F70A.MorphologicalImperative) => Phenomena.Directives.Typology.fromWALS70A✝ x.value) (Core.WALS.F70A.lookup "mnd") = some (some mandarin.morphImp)

theorem Phenomena.Directives.Typology.english_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "eng") = some english.prohibitive

theorem Phenomena.Directives.Typology.japanese_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "jpn") = some japanese.prohibitive

theorem Phenomena.Directives.Typology.mandarin_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "mnd") = some mandarin.prohibitive

theorem Phenomena.Directives.Typology.turkish_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "tur") = some turkish.prohibitive

theorem Phenomena.Directives.Typology.russian_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "rus") = some russian.prohibitive

theorem Phenomena.Directives.Typology.hindiUrdu_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "hin") = some hindiUrdu.prohibitive

theorem Phenomena.Directives.Typology.tagalog_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "tag") = some tagalog.prohibitive

theorem Phenomena.Directives.Typology.italian_ch71 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F71A.Prohibitive) => Phenomena.Directives.Typology.fromWALS71A✝ x.value) (Core.WALS.F71A.lookup "ita") = some italian.prohibitive

theorem Phenomena.Directives.Typology.english_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "eng") = some (some english.impHortSystem)

theorem Phenomena.Directives.Typology.japanese_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "jpn") = some (some japanese.impHortSystem)

theorem Phenomena.Directives.Typology.mandarin_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "mnd") = some (some mandarin.impHortSystem)

theorem Phenomena.Directives.Typology.turkish_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "tur") = some (some turkish.impHortSystem)

theorem Phenomena.Directives.Typology.finnish_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "fin") = some (some finnish.impHortSystem)

theorem Phenomena.Directives.Typology.russian_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "rus") = some (some russian.impHortSystem)

theorem Phenomena.Directives.Typology.swahili_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "swa") = some (some swahili.impHortSystem)

theorem Phenomena.Directives.Typology.tagalog_ch72 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F72A.ImperativeHortativeSystems) => Phenomena.Directives.Typology.fromWALS72A✝ x.value) (Core.WALS.F72A.lookup "tag") = some (some tagalog.impHortSystem)

theorem Phenomena.Directives.Typology.english_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "eng") = some (english.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.japanese_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "jpn") = some (japanese.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.mandarin_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "mnd") = some (mandarin.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.finnish_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "fin") = some (finnish.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.russian_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "rus") = some (russian.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.georgian_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "geo") = some (georgian.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.hindiUrdu_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "hin") = some (hindiUrdu.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.hungarian_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "hun") = some (hungarian.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.korean_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "kor") = some (korean.optative.getD OptativePresence.absent)

theorem Phenomena.Directives.Typology.swahili_ch73 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F73A.Optative) => Phenomena.Directives.Typology.fromWALS73A✝ x.value) (Core.WALS.F73A.lookup "swa") = some (swahili.optative.getD OptativePresence.absent)