Sentence Polarity

Binary sentence polarity: positive (affirmative) vs negative.

Used across phenomena involving polarity-sensitive behavior: multiplicity inferences, homogeneity gaps, scalar implicatures, etc.

Note: This is distinct from other polarity-like distinctions in the library:

• Core.Lexical.UD.Polarity — morphological feature (.Pos/.Neg)
• Core.NaturalLogic.ContextPolarity — monotonicity direction (.upward/.downward)
• Pragmatics.Implicature.Evaluativity.Polarity — adjective markedness
• Semantics.Presupposition.OntologicalPreconditions.Polarity — event assertion (.affirmed/.negated)

inductive Core.Polarity : Type

Sentence polarity: whether a sentence is affirmative or negated.

• positive : Polarity
• negative : Polarity

instance Core.instReprPolarity : Repr Polarity

Equations

• Core.instReprPolarity = { reprPrec := Core.instReprPolarity.repr }

def Core.instReprPolarity.repr : Polarity → Nat → Std.Format

Equations

• Core.instReprPolarity.repr Core.Polarity.positive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Polarity.positive")).group prec✝
• Core.instReprPolarity.repr Core.Polarity.negative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Polarity.negative")).group prec✝

instance Core.instDecidableEqPolarity : DecidableEq Polarity

Equations

• Core.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instBEqPolarity.beq : Polarity → Polarity → Bool

Equations

• Core.instBEqPolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.instBEqPolarity : BEq Polarity

Equations

• Core.instBEqPolarity = { beq := Core.instBEqPolarity.beq }

def Core.instInhabitedPolarity.default : Polarity

Equations

• Core.instInhabitedPolarity.default = Core.Polarity.positive

instance Core.instInhabitedPolarity : Inhabited Polarity

Equations

• Core.instInhabitedPolarity = { default := Core.instInhabitedPolarity.default }