Expressive

[Pot07] [Kub26]

Theory-neutral per-entry tag for use-conditional / secondary-meaning lexemes — the expressive dimension of [Pot07]. Fragments attach an Expressive value to mark a lexeme as expressive and record which construction class it belongs to; theories then assign it a denotation (Pragmatics.Expressives.TwoDimProp, an outlook-indexed meaning, use-conditional types, …) and are judged on whether they predict its diagnostic behavior.

This is object-level data (like Features.Person, Features.Evidentiality): a tag, not a denotation. It is Prop-free and depends on no theory layer, so Fragments may import it without pulling in any account of conventional implicature. The diagnostic fingerprint (Pragmatics.Expressives.SecondaryMeaningProperties) and the denotations live one layer up.

inductive Features.Expressive : Type

Construction class of a use-conditional / expressive lexeme ([Pot07], [Kub26]). The coarse, theory-neutral typology Fragments mark entries with.

• epithet : Expressive

  Epithets, slurs, and expressive adjectives — speaker-oriented affective content ("that bastard", "damn") ([Pot07]).

• honorific : Expressive

  Addressee- or referent-honorifics.

• supplement : Expressive

  Appositives and non-restrictive modifiers — Potts's supplements.

• outlookMarker : Expressive

  Discourse-sensitive evaluative particles / outlook markers ([Kub26]).

@[implicit_reducible]

instance Features.instDecidableEqExpressive : DecidableEq Expressive

Equations

• Features.instDecidableEqExpressive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.instReprExpressive : Repr Expressive

Equations

• Features.instReprExpressive = { reprPrec := Features.instReprExpressive.repr }

def Features.instReprExpressive.repr : Expressive → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instInhabitedExpressive : Inhabited Expressive

Equations

• Features.instInhabitedExpressive = { default := Features.instInhabitedExpressive.default }