Safe Haskell	Safe
Language	Haskell2010

Algebra.Heyting.Free.Expr

Synopsis

data Expr a
- = Var a
- | Bottom
- | Top
- | ( Expr a) :/\: ( Expr a)
- | ( Expr a) :\/: ( Expr a)
- | ( Expr a) :=>: ( Expr a)
proofSearch :: forall a. Ord a => Expr a -> Bool

Documentation

data Expr a Source #

Heyting algebra expression.

Note: this type doesn't have Heyting instance, as its Eq and Ord are structural.

Constructors

Var a
Bottom
Top
( Expr a) :/\: ( Expr a) infixr 6
( Expr a) :\/: ( Expr a) infixr 5
( Expr a) :=>: ( Expr a) infixr 4

Instances

Instances details

Monad Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods (>>=) :: Expr a -> (a -> Expr b) -> Expr b Source # (>>) :: Expr a -> Expr b -> Expr b Source # return :: a -> Expr a Source #
Functor Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods fmap :: (a -> b) -> Expr a -> Expr b Source # (<$) :: a -> Expr b -> Expr a Source #
Applicative Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods pure :: a -> Expr a Source # (<>) :: Expr (a -> b) -> Expr a -> Expr b Source # liftA2 :: (a -> b -> c) -> Expr a -> Expr b -> Expr c Source # (>) :: Expr a -> Expr b -> Expr b Source # (<*) :: Expr a -> Expr b -> Expr a Source #
Foldable Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods fold :: Monoid m => Expr m -> m Source # foldMap :: Monoid m => (a -> m) -> Expr a -> m Source # foldMap' :: Monoid m => (a -> m) -> Expr a -> m Source # foldr :: (a -> b -> b) -> b -> Expr a -> b Source # foldr' :: (a -> b -> b) -> b -> Expr a -> b Source # foldl :: (b -> a -> b) -> b -> Expr a -> b Source # foldl' :: (b -> a -> b) -> b -> Expr a -> b Source # foldr1 :: (a -> a -> a) -> Expr a -> a Source # foldl1 :: (a -> a -> a) -> Expr a -> a Source # toList :: Expr a -> [a] Source # null :: Expr a -> Bool Source # length :: Expr a -> Int Source # elem :: Eq a => a -> Expr a -> Bool Source # maximum :: Ord a => Expr a -> a Source # minimum :: Ord a => Expr a -> a Source # sum :: Num a => Expr a -> a Source # product :: Num a => Expr a -> a Source #
Traversable Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods traverse :: Applicative f => (a -> f b) -> Expr a -> f ( Expr b) Source # sequenceA :: Applicative f => Expr (f a) -> f ( Expr a) Source # mapM :: Monad m => (a -> m b) -> Expr a -> m ( Expr b) Source # sequence :: Monad m => Expr (m a) -> m ( Expr a) Source #
Eq a => Eq ( Expr a) Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods (==) :: Expr a -> Expr a -> Bool Source # (/=) :: Expr a -> Expr a -> Bool Source #
Data a => Data ( Expr a) Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods gfoldl :: ( forall d b. Data d => c (d -> b) -> d -> c b) -> ( forall g. g -> c g) -> Expr a -> c ( Expr a) Source # gunfold :: ( forall b r. Data b => c (b -> r) -> c r) -> ( forall r. r -> c r) -> Constr -> c ( Expr a) Source # toConstr :: Expr a -> Constr Source # dataTypeOf :: Expr a -> DataType Source # dataCast1 :: Typeable t => ( forall d. Data d => c (t d)) -> Maybe (c ( Expr a)) Source # dataCast2 :: Typeable t => ( forall d e. ( Data d, Data e) => c (t d e)) -> Maybe (c ( Expr a)) Source # gmapT :: ( forall b. Data b => b -> b) -> Expr a -> Expr a Source # gmapQl :: (r -> r' -> r) -> r -> ( forall d. Data d => d -> r') -> Expr a -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> ( forall d. Data d => d -> r') -> Expr a -> r Source # gmapQ :: ( forall d. Data d => d -> u) -> Expr a -> [u] Source # gmapQi :: Int -> ( forall d. Data d => d -> u) -> Expr a -> u Source # gmapM :: Monad m => ( forall d. Data d => d -> m d) -> Expr a -> m ( Expr a) Source # gmapMp :: MonadPlus m => ( forall d. Data d => d -> m d) -> Expr a -> m ( Expr a) Source # gmapMo :: MonadPlus m => ( forall d. Data d => d -> m d) -> Expr a -> m ( Expr a) Source #
Ord a => Ord ( Expr a) Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods compare :: Expr a -> Expr a -> Ordering Source # (<) :: Expr a -> Expr a -> Bool Source # (<=) :: Expr a -> Expr a -> Bool Source # (>) :: Expr a -> Expr a -> Bool Source # (>=) :: Expr a -> Expr a -> Bool Source # max :: Expr a -> Expr a -> Expr a Source # min :: Expr a -> Expr a -> Expr a Source #
Show a => Show ( Expr a) Source #
Instance details Defined in Algebra.Heyting.Free.Expr Methods showsPrec :: Int -> Expr a -> ShowS Source # show :: Expr a -> String Source # showList :: [ Expr a] -> ShowS Source #
Generic ( Expr a) Source #
Instance details Defined in Algebra.Heyting.Free.Expr Associated Types type Rep ( Expr a) :: Type -> Type Source # Methods from :: Expr a -> Rep ( Expr a) x Source # to :: Rep ( Expr a) x -> Expr a Source #
Generic1 Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr Associated Types type Rep1 Expr :: k -> Type Source # Methods from1 :: forall (a :: k). Expr a -> Rep1 Expr a Source # to1 :: forall (a :: k). Rep1 Expr a -> Expr a Source #
type Rep ( Expr a) Source #
Instance details Defined in Algebra.Heyting.Free.Expr type Rep ( Expr a) = D1 (' MetaData "Expr" "Algebra.Heyting.Free.Expr" "lattices-2.1-Aj77JapAM1ZIiO74F5gL5i" ' False ) (( C1 (' MetaCons "Var" ' PrefixI ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 a)) :+: ( C1 (' MetaCons "Bottom" ' PrefixI ' False ) ( U1 :: Type -> Type ) :+: C1 (' MetaCons "Top" ' PrefixI ' False ) ( U1 :: Type -> Type ))) :+: ( C1 (' MetaCons ":/\\:" (' InfixI ' RightAssociative 6) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Expr a)) :: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Expr a))) :+: ( C1 (' MetaCons ":\\/:" (' InfixI ' RightAssociative 5) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Expr a)) :: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Expr a))) :+: C1 (' MetaCons ":=>:" (' InfixI ' RightAssociative 4) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Expr a)) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 ( Expr a))))))
type Rep1 Expr Source #
Instance details Defined in Algebra.Heyting.Free.Expr type Rep1 Expr = D1 (' MetaData "Expr" "Algebra.Heyting.Free.Expr" "lattices-2.1-Aj77JapAM1ZIiO74F5gL5i" ' False ) (( C1 (' MetaCons "Var" ' PrefixI ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) Par1 ) :+: ( C1 (' MetaCons "Bottom" ' PrefixI ' False ) ( U1 :: Type -> Type ) :+: C1 (' MetaCons "Top" ' PrefixI ' False ) ( U1 :: Type -> Type ))) :+: ( C1 (' MetaCons ":/\\:" (' InfixI ' RightAssociative 6) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Expr ) :: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Expr )) :+: ( C1 (' MetaCons ":\\/:" (' InfixI ' RightAssociative 5) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Expr ) :: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Expr )) :+: C1 (' MetaCons ":=>:" (' InfixI ' RightAssociative 4) ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Expr ) :*: S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec1 Expr )))))

proofSearch :: forall a. Ord a => Expr a -> Bool Source #

Decide whether x :: Expr a is provable.

Note: this doesn't construct a proof term, but merely returns a Bool .