Mirativity

[DeL97] [Aik04]

Mirativity is the grammatical category that marks whether the propositional content is expected or surprising to the speaker. [DeL97] introduced the term and argued — against earlier evidential-subsumption analyses — that mirativity is typologically independent of evidentiality: the two categories are often conveyed by overlapping morphology (e.g., Turkish -mIş), but they answer distinct questions ("what is the source of the evidence?" vs "is the content surprising?").

This module is intentionally separate from Features.Evidentiality to reflect that independence; bundling structures that combine source, authority, and mirativity (e.g. Semantics.Epistemicity.EpistemicProfile) import both.

inductive Features.Mirativity.MirativityValue : Type

Mirativity value: whether the propositional content aligns with speaker expectations.

• expected : MirativityValue

  Content is expected / non-newsworthy.

• unexpected : MirativityValue

  Content is surprising / newsworthy.

• neutral : MirativityValue

  No mirative marking; expectation is unspecified.

@[implicit_reducible]

instance Features.Mirativity.instDecidableEqMirativityValue : DecidableEq MirativityValue

Equations

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

def Features.Mirativity.instReprMirativityValue.repr : MirativityValue → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Mirativity.instReprMirativityValue : Repr MirativityValue

Equations

• Features.Mirativity.instReprMirativityValue = { reprPrec := Features.Mirativity.instReprMirativityValue.repr }

@[implicit_reducible]

instance Features.Mirativity.instInhabitedMirativityValue : Inhabited MirativityValue

Equations

• Features.Mirativity.instInhabitedMirativityValue = { default := Features.Mirativity.instInhabitedMirativityValue.default }