Clause contexts

This file defines Clause.Context, the [sadock-zwicky-1985] sentence types with the interrogative split into polar, alternative, and constituent subtypes. Clause.Embedding is the orthogonal embedding axis; Semantics.Mood.IllocutionaryMood, Semantics.Mood.ClauseType, and Features.ClauseForm are coarser cuts.

inductive Clause.Context : Type

A [sadock-zwicky-1985] sentence type, with interrogatives subtyped.

• declarative : Context
• polarInterrogative : Context
• alternativeInterrogative : Context

  Alternative question ("Is it A or B?").

• constituentInterrogative : Context

  Constituent (wh-) question.

• imperative : Context
• exclamative : Context

@[implicit_reducible]

instance Clause.instDecidableEqContext : DecidableEq Context

Equations

• Clause.instDecidableEqContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Clause.instReprContext.repr : Context → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Clause.instReprContext.repr Clause.Context.declarative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Context.declarative")).group prec✝
• Clause.instReprContext.repr Clause.Context.imperative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Context.imperative")).group prec✝
• Clause.instReprContext.repr Clause.Context.exclamative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Context.exclamative")).group prec✝

@[implicit_reducible]

instance Clause.instReprContext : Repr Context

Equations

• Clause.instReprContext = { reprPrec := Clause.instReprContext.repr }

def Clause.Context.IsInterrogative : Context → Prop

The interrogative cells.

Equations

• Clause.Context.polarInterrogative.IsInterrogative = True
• Clause.Context.alternativeInterrogative.IsInterrogative = True
• Clause.Context.constituentInterrogative.IsInterrogative = True
• x✝.IsInterrogative = False

@[implicit_reducible]

instance Clause.Context.instDecidablePredIsInterrogative : DecidablePred IsInterrogative

Equations

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