logic-classes-1.4.8: Framework for propositional and first order logic, theorem proving

Safe HaskellSafe-Inferred

Data.Logic.Classes.Negate

Synopsis

Documentation

class Negatable formula whereSource

The class of formulas that can be negated. There are some types that can be negated but do not support the other Boolean Logic operators, such as the Literal class.

Methods

negatePrivate :: formula -> formulaSource

Negate a formula in a naive fashion, the operators below prevent double negation.

foldNegationSource

Arguments

:: (formula -> r)

called for normal formulas

-> (formula -> r)

called for negated formulas

-> formula 
-> r 

Test whether a formula is negated or normal

negated :: Negatable formula => formula -> BoolSource

Is this formula negated at the top level?

(.~.) :: Negatable formula => formula -> formulaSource

Negate the formula, avoiding double negation

(¬) :: Negatable formula => formula -> formulaSource

negative :: Negatable formula => formula -> BoolSource

positive :: Negatable formula => formula -> BoolSource