Shared Slavic Verbal-Prefix Parameters #

[Sve04] [Ist04] [Jab04]

Types and parameters shared across Slavic verbal-prefix fragments (Russian, Polish, Bulgarian) following [Sve04]'s lexical / superlexical distinction. Mirrors the Fragments/Mayan/Params.lean pattern: shared cluster-level types factored out so per-language fragments don't triplicate them.

Aspect is reused from Linglib.Core.UD (UD-tag canonical Aspect.Imp / Aspect.Perf) rather than redefined per Slavic fragment.

Main definitions #

Aspect — perfective vs imperfective (binary distinction sufficient for Slavic; the richer UD-tagset Aspect enum lives in Linglib.Core.UD).
SuperlexicalSubtype — six aspectual subtypes (paper §3).
PrefixClass — lexical or superlexical _ ADT.
PrefixClass.IsSuperlexical predicate with DecidablePred instance.

Cross-references #

source

inductive Slavic.Aspect :

Type

Slavic grammatical aspect — the binary perfective / imperfective contrast.

perfective : Aspect
imperfective : Aspect

Instances For

source

@[implicit_reducible]

instance Slavic.instDecidableEqAspect :

DecidableEq Aspect

Equations

Slavic.instDecidableEqAspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

inductive Slavic.SuperlexicalSubtype :

Type

Aspectual subtypes for the superlexical class ([Sve04] §3). The same six categories used across Russian, Polish, and Bulgarian VPC fragments.

delimitative : SuperlexicalSubtype
cumulative : SuperlexicalSubtype
completive : SuperlexicalSubtype
repetitive : SuperlexicalSubtype
inceptive : SuperlexicalSubtype
distributive : SuperlexicalSubtype

Instances For

source

@[implicit_reducible]

instance Slavic.instDecidableEqSuperlexicalSubtype :

DecidableEq SuperlexicalSubtype

Equations

Slavic.instDecidableEqSuperlexicalSubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

inductive Slavic.PrefixClass :

Type

[Sve04]'s lexical / superlexical split as a single ADT — the superlexical case carries its subtype, eliminating the need for an Option-typed companion field plus a consistency lemma.