HyLo.Formula

Documentation

data Formula n p r

Constructors

Top

Bot

Prop p

Nom n

Neg (Formula n p r)

(Formula n p r) :&: (Formula n p r)

(Formula n p r) :|: (Formula n p r)

(Formula n p r) :-->: (Formula n p r)

(Formula n p r) :<-->: (Formula n p r)

Diam r (Formula n p r)

Box r (Formula n p r)

At n (Formula n p r)

A (Formula n p r)

E (Formula n p r)

D (Formula n p r)

B (Formula n p r)

Down n (Formula n p r)

Instances

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r, w) (Formula n p r) n p r

(Eq n, Eq p, Eq r) => Eq (Formula n p r)

(Ord n, Ord p, Ord r) => Ord (Formula n p r)

(Read n, Read p, Read r) => Read (Formula n p r)

(Show n, Show p, Show r) => Show (Formula n p r)

(Arbitrary n, Arbitrary p, Arbitrary r) => Arbitrary (Formula n p r)

Uniplate (Formula n p r)

(Ord n, Ord p, Ord r) => HasSignature (Formula n p r)

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r

nnf :: Formula n p r -> Formula n p r

composeFold :: b -> (b -> b -> b) -> (Formula n p r -> b) -> Formula n p r -> b

composeFoldM :: Monad m => m b -> (b -> b -> m b) -> (Formula n p r -> m b) -> Formula n p r -> m b

composeMap :: (Formula n p r -> Formula n p r) -> (Formula n p r -> Formula n p r) -> Formula n p r -> Formula n p r

composeMapM :: (Monad m, Functor m) => (Formula n p r -> m (Formula n p r)) -> (Formula n p r -> m (Formula n p r)) -> Formula n p r -> m (Formula n p r)

onShape :: (n -> n') -> (p -> p') -> (r -> r') -> (Formula n p r -> Formula n' p' r') -> Formula n p r -> Formula n' p' r'

mapSig :: (n -> n') -> (p -> p') -> (r -> r') -> Formula n p r -> Formula n' p' r'

freeVars :: Eq n => Formula n p r -> [n]

boundVars :: Eq n => Formula n p r -> [n]

type TestFormula = Formula NomSymbol PropSymbol RelSymbol

metap_read_Formula :: (Show n, Read n, Eq n, Show p, Read p, Eq p, Show r, Read r, Eq r) => Formula n p r -> Bool

unit_tests :: UnitTest