Classical Tibetan role particles

Classical Tibetan marks the role of a participant by a role particle after its noun phrase ([Bey92], p. 252): the patient by none, the agency, agent and instrument alike, by -KYis (p. 269, n. 15), a locus by -la, or by -na where the locus is an enclosed space, a source likewise by -las or -nas (pp. 268–269), and the accompaniment by -daŋ, the same form as the conjunction 'and' (p. 241, n. 47). A locus particle marks the site of a verb of location and the target of a verb of motion alike (p. 269).

Main definitions

• ClassicalTibetan.Case, ClassicalTibetan.Case.exponents: the role particles.
• ClassicalTibetan.Case.label, ClassicalTibetan.Case.functions: the comparative value each is named for, and the values it expresses.

Implementation notes

• -KYis is in Beyer's notation, capitals for the segments that assimilate to the noun.

References

• [Bey92]

inductive ClassicalTibetan.Case : Type

The role particles.

• patient : Case

  The patient, unmarked.

• agency : Case

  The agency, agent or instrument.

• locus : Case

  The locus.

• boundedLocus : Case

  The locus as an enclosed space.

• source : Case

  The source.

• boundedSource : Case

  The source as an enclosed space.

• accompaniment : Case

  The accompaniment.

@[instance_reducible]

instance ClassicalTibetan.instDecidableEqCase : DecidableEq Case

Equations

• ClassicalTibetan.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ClassicalTibetan.instFintypeCase : Fintype Case

Equations

• ClassicalTibetan.instFintypeCase = { elems := { val := ↑ClassicalTibetan.Case.enumList, nodup := ClassicalTibetan.Case.enumList_nodup }, complete := ClassicalTibetan.instFintypeCase._proof_1 }

def ClassicalTibetan.instReprCase.repr : Case → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ClassicalTibetan.instReprCase : Repr Case

Equations

• ClassicalTibetan.instReprCase = { reprPrec := ClassicalTibetan.instReprCase.repr }

def ClassicalTibetan.Case.label : Case → _root_.Case

The comparative value a particle is named for.

Equations

• ClassicalTibetan.Case.patient.label = Case.abs
• ClassicalTibetan.Case.agency.label = Case.erg
• ClassicalTibetan.Case.locus.label = Case.loc
• ClassicalTibetan.Case.boundedLocus.label = Case.loc
• ClassicalTibetan.Case.source.label = Case.abl
• ClassicalTibetan.Case.boundedSource.label = Case.abl
• ClassicalTibetan.Case.accompaniment.label = Case.com

def ClassicalTibetan.Case.functions : Case → Finset _root_.Case

The comparative values a particle expresses: the agency also the instrument, and a locus also the goal of motion.

Equations

• ClassicalTibetan.Case.agency.functions = {Case.erg, Case.inst}
• ClassicalTibetan.Case.locus.functions = {Case.loc, Case.all}
• ClassicalTibetan.Case.boundedLocus.functions = {Case.loc, Case.all}
• x✝.functions = {x✝.label}

theorem ClassicalTibetan.Case.label_mem_functions (c : Case) : c.label ∈ c.functions

def ClassicalTibetan.Case.exponents : Case → List Morphology.Morph

The role particle of a case.

Equations

• ClassicalTibetan.Case.patient.exponents = []
• ClassicalTibetan.Case.agency.exponents = [Morphology.Morph.encl "KYis"]
• ClassicalTibetan.Case.locus.exponents = [Morphology.Morph.encl "la"]
• ClassicalTibetan.Case.boundedLocus.exponents = [Morphology.Morph.encl "na"]
• ClassicalTibetan.Case.source.exponents = [Morphology.Morph.encl "las"]
• ClassicalTibetan.Case.boundedSource.exponents = [Morphology.Morph.encl "nas"]
• ClassicalTibetan.Case.accompaniment.exponents = [Morphology.Morph.encl "daŋ"]