Adjectival construction types

The surface constructions a gradable adjective participates in — positive, comparative, equative, measure phrase, degree question. Evaluativity analyses track which constructions trigger evaluative readings ([Ret15]); markedness implicature computes alternatives over them (Pragmatics/Implicature/Markedness.lean).

The degree-substrate DegP taxonomy (DegPType, covering degree heads rather than adjectival surface constructions) lives in Semantics/Degree/Defs.lean.

inductive Degree.AdjectivalConstruction : Type

Degree construction type. Used by evaluativity analyses to track which surface constructions trigger evaluative readings.

• positive : AdjectivalConstruction

  "Kim is tall" — unmarked form.

• comparative : AdjectivalConstruction

  "Kim is taller than Sam".

• equative : AdjectivalConstruction

  "Kim is as tall as Sam".

• measurePhrase : AdjectivalConstruction

  "Kim is 6 feet tall" — explicit measure phrase.

• degreeQuestion : AdjectivalConstruction

  "How tall is Kim?".

def Degree.instReprAdjectivalConstruction.repr : AdjectivalConstruction → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instReprAdjectivalConstruction : Repr AdjectivalConstruction

Equations

• Degree.instReprAdjectivalConstruction = { reprPrec := Degree.instReprAdjectivalConstruction.repr }

@[implicit_reducible]

instance Degree.instDecidableEqAdjectivalConstruction : DecidableEq AdjectivalConstruction

Equations

• Degree.instDecidableEqAdjectivalConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instToStringAdjectivalConstruction : ToString AdjectivalConstruction

User-facing rendering, distinct from Repr (which prefixes the namespace). Consumed by Studies files that string-interpolate construction names into diagnostic messages — see e.g. Studies/Rett2015Implicature.lean.

Equations

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