Degree constructions

This file defines Degree.Construction, the surface forms a gradable predicate can appear in — bare positive, comparative, equative, measure phrase, and degree question ([beck-2011], [Ret15]). The Deg⁰ head inventory is defined in Linglib/Syntax/Category/Degree/Basic.lean.

inductive Degree.Construction : Type

A surface degree construction built on a gradable predicate.

• positive : Construction

  "Kim is tall" — unmarked form.

• comparative : Construction

  "Kim is taller than Sam".

• equative : Construction

  "Kim is as tall as Sam".

• measurePhrase : Construction

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

• degreeQuestion : Construction

  "How tall is Kim?".

@[instance_reducible]

instance Degree.instDecidableEqConstruction : DecidableEq Construction

Equations

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

def Degree.instReprConstruction.repr : Construction → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Degree.instReprConstruction : Repr Construction

Equations

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

@[instance_reducible]

instance Degree.instToStringConstruction : ToString Construction

Bare lowercase construction names for diagnostic messages, distinct from Repr (which prefixes the namespace).

Equations

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