The degree head (Deg)

This file defines Degree.Head, the inventory of the functional category Deg that heads the adjectival extended projection ([abney-1987]; [corver-1997]). The comparison heads are surveyed in [beck-2011]; the too ~ enough pair belongs to the sufficiency-excess literature ([Mei03]).

inductive Degree.Head : Type

The Deg⁰ inventory of a Degree Phrase. The phrase's internal structure is framework-dependent — [Ken99] posits a than-clause complement to Deg, [Hei00] a scopal degree operator — but the head inventory itself is framework-independent.

• comparative : Head

  -er / more.

• equative : Head

  as...as.

• superlative : Head

  -est / most.

• excessive : Head

  too.

• sufficiency : Head

  enough.

@[instance_reducible]

instance Degree.instDecidableEqHead : DecidableEq Head

Equations

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

def Degree.instReprHead.repr : Head → Nat → Std.Format

Equations

• Degree.instReprHead.repr Degree.Head.comparative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Head.comparative")).group prec✝
• Degree.instReprHead.repr Degree.Head.equative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Head.equative")).group prec✝
• Degree.instReprHead.repr Degree.Head.superlative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Head.superlative")).group prec✝
• Degree.instReprHead.repr Degree.Head.excessive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Head.excessive")).group prec✝
• Degree.instReprHead.repr Degree.Head.sufficiency prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Degree.Head.sufficiency")).group prec✝

@[instance_reducible]

instance Degree.instReprHead : Repr Head

Equations

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