Tanti Dargwa verbs

This file defines the light verbs and complex verbs of Tanti Dargwa as Sumbatova describes them. A Dargwa verb is simplex, a bare root with at most a gender prefix, a preverb verb, or a complex verb, a lexical stem followed by a light verb with any preverbs between them. The lexical stems are noun, adjective, numeral, verb or ideophone stems, some of them found only in the complex verb, and a few light verbs likewise occur only there. The valency alternations of the verb are in Voice.lean.

Main definitions

• Dargwa.LightVerb, Dargwa.lightVerbs: the light verbs, each with the meaning of the homophonous simplex verb where it has one
• Dargwa.ComplexVerb: a lexical stem, as a Semantics.Root, with its word class, preverbs and light verb

Implementation notes

• A light verb is cited by its stem without the gender prefix, agrees recording the roots whose shape begins with the agreement slot. Sumbatova lists aq- both as 'hang' and among the light verbs found only in complex verbs; both entries are kept.
• The Muira Dargwa complex predicates of Kalyakin's study, with the position he assigns their roots, are in Studies/Kalyakin2026.lean.

References

• N. Sumbatova, Dargwa (2021)

Light verbs

structure Dargwa.LightVerb : Type

A light verb is the verbal component of a complex verb.

• stem : String

  The stem, without the gender prefix.

• agrees : Bool

  Whether the root begins with the gender agreement slot.

• heavy : Option String

  The meaning of the homophonous simplex verb, none for a light verb found only in complex verbs.

def Dargwa.instDecidableEqLightVerb.decEq (x✝ x✝¹ : LightVerb) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Dargwa.instDecidableEqLightVerb : DecidableEq LightVerb

Equations

• Dargwa.instDecidableEqLightVerb = Dargwa.instDecidableEqLightVerb.decEq

@[instance_reducible]

instance Dargwa.instReprLightVerb : Repr LightVerb

Equations

• Dargwa.instReprLightVerb = { reprPrec := Dargwa.instReprLightVerb.repr }

def Dargwa.instReprLightVerb.repr : LightVerb → ℕ → Std.Format

Equations

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

def Dargwa.make : LightVerb

b-arq'- 'do, make', the most common light verb.

Equations

• Dargwa.make = { stem := "arq'", agrees := true, heavy := some "do, make" }

def Dargwa.become : LightVerb

b-iχ- 'become'.

Equations

• Dargwa.become = { stem := "iχ", agrees := true, heavy := some "become" }

def Dargwa.speak : LightVerb

w-ik'- 'speak'.

Equations

• Dargwa.speak = { stem := "ik'", agrees := true, heavy := some "speak" }

def Dargwa.leave : LightVerb

b-at- 'leave'.

Equations

• Dargwa.leave = { stem := "at", agrees := true, heavy := some "leave" }

def Dargwa.fall : LightVerb

b-ič- 'fall'.

Equations

• Dargwa.fall = { stem := "ič", agrees := true, heavy := some "fall" }

def Dargwa.hit : LightVerb

b-aˁq- 'hit'.

Equations

• Dargwa.hit = { stem := "aˁq", agrees := true, heavy := some "hit" }

def Dargwa.standUp : LightVerb

b-icː- 'stand up'.

Equations

• Dargwa.standUp = { stem := "icː", agrees := true, heavy := some "stand up" }

def Dargwa.sitDown : LightVerb

b-ig- 'sit down'.

Equations

• Dargwa.sitDown = { stem := "ig", agrees := true, heavy := some "sit down" }

def Dargwa.hang : LightVerb

aq- 'hang'.

Equations

• Dargwa.hang = { stem := "aq", agrees := false, heavy := some "hang" }

def Dargwa.reach : LightVerb

aʁ- 'reach'.

Equations

• Dargwa.reach = { stem := "aʁ", agrees := false, heavy := some "reach" }

def Dargwa.come : LightVerb

b-ač'- 'come'.

Equations

• Dargwa.come = { stem := "ač'", agrees := true, heavy := some "come" }

def Dargwa.comeHere : LightVerb

le-b-q'- 'come (here)'.

Equations

• Dargwa.comeHere = { stem := "le-q'", agrees := true, heavy := some "come (here)" }

def Dargwa.collect : LightVerb

b-arʁ- 'collect'.

Equations

• Dargwa.collect = { stem := "arʁ", agrees := true, heavy := some "collect" }

def Dargwa.put : LightVerb

b-ixː- 'put'.

Equations

• Dargwa.put = { stem := "ixː", agrees := true, heavy := some "put" }

def Dargwa.beat : LightVerb

it- 'beat'.

Equations

• Dargwa.beat = { stem := "it", agrees := false, heavy := some "beat" }

def Dargwa.goAway : LightVerb

ag- 'go away'.

Equations

• Dargwa.goAway = { stem := "ag", agrees := false, heavy := some "go away" }

def Dargwa.say : LightVerb

ʔ- 'say'.

Equations

• Dargwa.say = { stem := "ʔ", agrees := false, heavy := some "say" }

def Dargwa.drive : LightVerb

b-erk'- 'drive'.

Equations

• Dargwa.drive = { stem := "erk'", agrees := true, heavy := some "drive" }

def Dargwa.sift : LightVerb

arg- 'sift'.

Equations

• Dargwa.sift = { stem := "arg", agrees := false, heavy := some "sift" }

def Dargwa.tear : LightVerb

b-ertː- 'tear'.

Equations

• Dargwa.tear = { stem := "ertː", agrees := true, heavy := some "tear" }

def Dargwa.struggle : LightVerb

b-aˁʜ- 'struggle'.

Equations

• Dargwa.struggle = { stem := "aˁʜ", agrees := true, heavy := some "struggle" }

def Dargwa.cut : LightVerb

b-ut'- 'cut', the light verb of č'u-b-ut'- 'divide by two'.

Equations

• Dargwa.cut = { stem := "ut'", agrees := true, heavy := some "cut" }

def Dargwa.uq : LightVerb

b-uq-, found only in complex verbs.

Equations

• Dargwa.uq = { stem := "uq", agrees := true, heavy := none }

def Dargwa.aq : LightVerb

aq-, found only in complex verbs.

Equations

• Dargwa.aq = { stem := "aq", agrees := false, heavy := none }

def Dargwa.ikk : LightVerb

b-ikː-, found only in complex verbs.

Equations

• Dargwa.ikk = { stem := "ikː", agrees := true, heavy := none }

def Dargwa.art : LightVerb

art-, found only in complex verbs.

Equations

• Dargwa.art = { stem := "art", agrees := false, heavy := none }

def Dargwa.lightVerbs : Finset LightVerb

The light verbs Sumbatova lists.

Equations

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

Complex verbs

inductive Dargwa.StemClass : Type

The word class of the lexical stem of a complex verb as an independent word.

• noun : StemClass
• adjective : StemClass
• numeral : StemClass
• verb : StemClass
• ideophone : StemClass

@[instance_reducible]

instance Dargwa.instDecidableEqStemClass : DecidableEq StemClass

Equations

• Dargwa.instDecidableEqStemClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dargwa.instReprStemClass : Repr StemClass

Equations

• Dargwa.instReprStemClass = { reprPrec := Dargwa.instReprStemClass.repr }

def Dargwa.instReprStemClass.repr : StemClass → ℕ → Std.Format

Equations

• Dargwa.instReprStemClass.repr Dargwa.StemClass.noun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.StemClass.noun")).group prec✝
• Dargwa.instReprStemClass.repr Dargwa.StemClass.adjective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.StemClass.adjective")).group prec✝
• Dargwa.instReprStemClass.repr Dargwa.StemClass.numeral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.StemClass.numeral")).group prec✝
• Dargwa.instReprStemClass.repr Dargwa.StemClass.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.StemClass.verb")).group prec✝
• Dargwa.instReprStemClass.repr Dargwa.StemClass.ideophone prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dargwa.StemClass.ideophone")).group prec✝

@[instance_reducible]

instance Dargwa.instFintypeStemClass : Fintype StemClass

Equations

• Dargwa.instFintypeStemClass = { elems := { val := ↑Dargwa.StemClass.enumList, nodup := Dargwa.StemClass.enumList_nodup }, complete := Dargwa.instFintypeStemClass._proof_1 }

structure Dargwa.ComplexVerb : Type

A complex verb is a lexical stem, cited as the root it contributes, followed by a light verb, with any preverbs between them.

• root : Semantics.Root

  The lexical stem, which carries the core meaning of the complex.

• category : Option StemClass

  The word class of the stem, none for a stem restricted to the complex verb.

• preverbs : List Morphology.Morph

  The preverbs between the stem and the light verb.

• lightVerb : LightVerb

  The light verb.

• gloss : String

  The meaning of the complex verb.

def Dargwa.instDecidableEqComplexVerb.decEq (x✝ x✝¹ : ComplexVerb) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Dargwa.instDecidableEqComplexVerb : DecidableEq ComplexVerb

Equations

• Dargwa.instDecidableEqComplexVerb = Dargwa.instDecidableEqComplexVerb.decEq

@[instance_reducible]

instance Dargwa.instReprComplexVerb : Repr ComplexVerb

Equations

• Dargwa.instReprComplexVerb = { reprPrec := Dargwa.instReprComplexVerb.repr }

def Dargwa.instReprComplexVerb.repr : ComplexVerb → ℕ → Std.Format

Equations

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

def Dargwa.finish : ComplexVerb

taman-b-arq'- 'finish' (transitive), from taman 'end'.

Equations

• Dargwa.finish = { root := { name := "taman" }, category := some Dargwa.StemClass.noun, lightVerb := Dargwa.make, gloss := "finish" }

def Dargwa.prepare : ComplexVerb

ʜaˁdur-d-arq'- 'prepare', from ʜaˁdur- 'ready'.

Equations

• Dargwa.prepare = { root := { name := "ʜaˁdur" }, category := some Dargwa.StemClass.adjective, lightVerb := Dargwa.make, gloss := "prepare" }

def Dargwa.divideByTwo : ComplexVerb

č'u-b-ut'- 'divide by two', from č'u 'two'.

Equations

• Dargwa.divideByTwo = { root := { name := "č'u" }, category := some Dargwa.StemClass.numeral, lightVerb := Dargwa.cut, gloss := "divide by two" }

def Dargwa.cough : ComplexVerb

qeʜ-w-ik'- 'cough' (imperfective), from the ideophone qeʜ-.

Equations

• Dargwa.cough = { root := { name := "qeʜ" }, category := some Dargwa.StemClass.ideophone, lightVerb := Dargwa.speak, gloss := "cough" }

def Dargwa.startCrying : ComplexVerb

w-isːe-w-ig- 'start crying', from w-isː- 'cry' (imperfective).

Equations

• Dargwa.startCrying = { root := { name := "isːe" }, category := some Dargwa.StemClass.verb, lightVerb := Dargwa.sitDown, gloss := "start crying" }

def Dargwa.spin : ComplexVerb

tːurχ-b-arq'- 'spin', from a stem found nowhere else.

Equations

• Dargwa.spin = { root := { name := "tːurχ" }, category := none, lightVerb := Dargwa.make, gloss := "spin" }

def Dargwa.stop : ComplexVerb

t'aš-ka-b-icː- 'stop', from a stem found nowhere else, with the preverb ka- 'downward' between it and the light verb.

Equations

• Dargwa.stop = { root := { name := "t'aš" }, category := none, preverbs := [Morphology.Morph.pref "ka"], lightVerb := Dargwa.standUp, gloss := "stop" }