Data.Logic.ATP.LitWrapper

Documentation

data JL a

Wrapper type to make an IsLiteral value that happens to also be JustLiteral. The JL constructor is not exported, JL values can be built using convertToLiteral.

Instances

IsLiteral a => IsFormula (JL a)

Defined in Data.Logic.ATP.LitWrapper

Associated Types

type AtomOf (JL a)

Methods

true :: JL a

false :: JL a

asBool :: JL a -> Maybe Bool

atomic :: AtomOf (JL a) -> JL a

overatoms :: (AtomOf (JL a) -> r -> r) -> JL a -> r -> r

onatoms :: (AtomOf (JL a) -> AtomOf (JL a)) -> JL a -> JL a

(IsFormula (JL a), IsLiteral a) => IsLiteral (JL a)

Defined in Data.Logic.ATP.LitWrapper

Methods

naiveNegate :: JL a -> JL a

foldNegation :: (JL a -> r) -> (JL a -> r) -> JL a -> r

foldLiteral' :: (JL a -> r) -> (JL a -> r) -> (Bool -> r) -> (AtomOf (JL a) -> r) -> JL a -> r

(IsFormula (JL a), IsLiteral a) => JustLiteral (JL a)

Defined in Data.Logic.ATP.LitWrapper

HasFixity a => HasFixity (JL a)

Defined in Data.Logic.ATP.LitWrapper

Methods

precedence :: JL a -> Precedence

associativity :: JL a -> Associativity

Pretty a => Pretty (JL a)

Defined in Data.Logic.ATP.LitWrapper

Methods

pPrintPrec :: PrettyLevel -> Rational -> JL a -> Doc

pPrint :: JL a -> Doc

pPrintList :: PrettyLevel -> [JL a] -> Doc

type AtomOf (JL a)

Defined in Data.Logic.ATP.LitWrapper

type AtomOf (JL a) = AtomOf a