Clause-embedding adjectives

Adjectives that take propositional complements — annoyed (that p), sorry (that p), aware (that p), certain (that p). On the pattern of GradableAdjective in Semantics/Gradability, ClauseEmbeddingAdjective extends the Adjective core with the clausal-selection spine it shares with clause-embedding verbs: complement type, presupposition trigger class, attitude, opacity, and entailment signature.

Whether predication requires a copula is a language-level property ([Sta13b]), not a property of the adjective: English realizes these predicates as be + adjective (ClauseEmbeddingAdjective.toVerb in Fragments/English/Predicates/Copular.lean), Mandarin and Japanese without a copula.

structure ClauseEmbeddingAdjectiveextends Adjective : Type

A clause-embedding adjective: the Adjective core plus the clausal-selection spine shared with clause-embedding verbs, but no verbal morphology.

• form : String
• script : Option String
• dimension : Option Features.ScalarDimension
• isLowerEndpoint : Bool
• polarity : Option Core.Order.ScalePolarity
• comparison : ComparisonFacet
• antonymForm : Option String
• complementType : ComplementType

  What kind of clause the adjective embeds.

• presupType : Option PresupTriggerType

  Presupposition trigger class, if the adjective is a trigger.

• attitude : Option Features.Attitude

  Attitude semantics, if applicable.

• opaqueContext : Bool

  Does the adjective create an opaque context?

• complementSig : Option NaturalLogic.Signature

  Entailment signature of the complement position.

def instReprClauseEmbeddingAdjective.repr : ClauseEmbeddingAdjective → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprClauseEmbeddingAdjective : Repr ClauseEmbeddingAdjective

Equations

• instReprClauseEmbeddingAdjective = { reprPrec := instReprClauseEmbeddingAdjective.repr }

@[instance_reducible]

instance instBEqClauseEmbeddingAdjective : BEq ClauseEmbeddingAdjective

Equations

• instBEqClauseEmbeddingAdjective = { beq := instBEqClauseEmbeddingAdjective.beq }

def instBEqClauseEmbeddingAdjective.beq : ClauseEmbeddingAdjective → ClauseEmbeddingAdjective → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqClauseEmbeddingAdjective.beq x✝¹ x✝ = false