Standard negation

A language negates a declarative verbal main clause with a marker: an affix on the verb, a free particle, an inflecting negative verb, or two morphemes at once (French ne … pas). A negative may differ from its affirmative only by the marker, or the clause may also change, taking a nonfinite verb form or losing tense distinctions, the divide Miestamo calls symmetric and asymmetric.

Main declarations

• Negation.Marker: a standard negation marker, as the morphs exponing it.

Implementation notes

A typology of markers or of negative constructions is one author's classification and lives in that author's study, such as Miestamo's symmetry in Studies/Miestamo2005.lean, whose affirmative–negative pairs are its example rows. An inflecting negative verb is cited by its stem, and its endings form an Agreement.Paradigm in the language's fragment.

References

• [Mie05]

structure Negation.Marker : Type

A standard sentential negation marker.

• pieces : List (List Morphology.Morph)

  The exponent as contiguous pieces in surface order; a bipartite marker has two (Burmese ma-…-bu). Affixal alternants are recorded by an abstract citation form (Turkish -mA- for -ma- ~ -me-).

def Negation.instDecidableEqMarker.decEq (x✝ x✝¹ : Marker) : Decidable (x✝ = x✝¹)

Equations

• Negation.instDecidableEqMarker.decEq { pieces := a } { pieces := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Negation.instDecidableEqMarker : DecidableEq Marker

Equations

• Negation.instDecidableEqMarker = Negation.instDecidableEqMarker.decEq

def Negation.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Negation.instReprMarker : Repr Marker

Equations

• Negation.instReprMarker = { reprPrec := Negation.instReprMarker.repr }

def Negation.Marker.form (m : Marker) : String

The surface form of a marker is its pieces in boundary notation, separated by ….

Equations

• m.form = "…".intercalate (List.map Morphology.Morph.surface m.pieces)

def Negation.Marker.morphs (m : Marker) : List Morphology.Morph

The morphs of a marker, across its pieces.

Equations

• m.morphs = m.pieces.flatten