Refinery.Tactic

Documentation

data TacticT jdg ext m a

A TacticT is a monad transformer that performs proof refinement. The type variables signifiy:

• jdg - The goal type. This is the thing we are trying to construct a proof of.
• ext - The extract type. This is what we will recieve after running the tactic.
• m - The base monad.
• a - The return value. This to make TacticT a monad, and will always be '()'

Instances

(MonadProvable jdg m, MonadState s m) => MonadState s (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

get :: TacticT jdg ext m s

put :: s -> TacticT jdg ext m ()

state :: (s -> (a, s)) -> TacticT jdg ext m a

(MonadReader env m, MonadProvable jdg m) => MonadReader env (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

ask :: TacticT jdg ext m env

local :: (env -> env) -> TacticT jdg ext m a -> TacticT jdg ext m a

reader :: (env -> a) -> TacticT jdg ext m a

(MonadError err m, MonadProvable jdg m) => MonadError err (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

throwError :: err -> TacticT jdg ext m a

catchError :: TacticT jdg ext m a -> (err -> TacticT jdg ext m a) -> TacticT jdg ext m a

MonadTrans (TacticT jdg ext)

Defined in Refinery.Tactic.Internal

Methods

lift :: Monad m => m a -> TacticT jdg ext m a

MonadProvable jdg m => Monad (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: TacticT jdg ext m a -> (a -> TacticT jdg ext m b) -> TacticT jdg ext m b

(>>) :: TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m b

return :: a -> TacticT jdg ext m a

fail :: String -> TacticT jdg ext m a

Monad m => Functor (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

fmap :: (a -> b) -> TacticT jdg ext m a -> TacticT jdg ext m b

(<$) :: a -> TacticT jdg ext m b -> TacticT jdg ext m a

MonadProvable jdg m => Applicative (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

pure :: a -> TacticT jdg ext m a

(<*>) :: TacticT jdg ext m (a -> b) -> TacticT jdg ext m a -> TacticT jdg ext m b

liftA2 :: (a -> b -> c) -> TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m c

(*>) :: TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m b

(<*) :: TacticT jdg ext m a -> TacticT jdg ext m b -> TacticT jdg ext m a

(MonadIO m, MonadProvable jdg m) => MonadIO (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> TacticT jdg ext m a

(MonadThrow m, MonadProvable jdg m) => MonadThrow (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

throwM :: Exception e => e -> TacticT jdg ext m a

(MonadCatch m, MonadProvable jdg m) => MonadCatch (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

catch :: Exception e => TacticT jdg ext m a -> (e -> TacticT jdg ext m a) -> TacticT jdg ext m a

MonadError err m => Alt (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(<!>) :: TacticT jdg ext m a -> TacticT jdg ext m a -> TacticT jdg ext m a

some :: Applicative (TacticT jdg ext m) => TacticT jdg ext m a -> TacticT jdg ext m [a]

many :: Applicative (TacticT jdg ext m) => TacticT jdg ext m a -> TacticT jdg ext m [a]

runTacticT :: MonadExtract ext m => TacticT jdg ext m () -> jdg -> m (ext, [jdg])

Runs a tactic, producing the extract, along with a list of unsolved subgoals.

Tactic Combinators

(<@>) :: MonadProvable jdg m => TacticT jdg ext m () -> [TacticT jdg ext m ()] -> TacticT jdg ext m ()

Create a tactic that applies each of the tactics in the list to one subgoal.

When the number of subgoals is greater than the number of provided tactics, the identity tactic is applied to the remainder. When the number of subgoals is less than the number of provided tactics, the remaining tactics are ignored.

try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()

Tries to run a tactic, backtracking on failure

many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()

Runs a tactic repeatedly until it fails

choice :: (MonadProvable jdg m, MonadError err m) => err -> [TacticT jdg ext m a] -> TacticT jdg ext m a

choice err ts tries to apply a series of tactics ts, and commits to the 1st tactic that succeeds. If they all fail, then err is thrown

progress :: (MonadProvable jdg m, MonadError err m) => (jdg -> jdg -> Bool) -> err -> TacticT jdg ext m a -> TacticT jdg ext m a

progress eq err t applies the tactic t, and checks to see if the resulting subgoals are all equal to the initial goal by using eq. If they are, it throws err.

Subgoal Manipulation

goal :: Monad m => TacticT jdg ext m jdg

Get the current goal

focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () -> Int -> TacticT jdg ext m () -> TacticT jdg ext m ()

Apply the first tactic, and then apply the second tactic focused on the nth subgoal.

forSubgoals :: Monad m => TacticT jdg ext m a -> (jdg -> m b) -> TacticT jdg ext m a

Applies f to every subgoals resulting from the tactic t.

Tactic Creation

class Monad m => MonadExtract ext m | m -> ext where

Minimal complete definition

Nothing

Methods

hole :: m ext

Generates a "hole" of type ext, which should represent an incomplete extract.

hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext

Generates a "hole" of type ext, which should represent an incomplete extract.

Instances

MonadExtract ext m => MonadExtract ext (ExceptT err m)

Defined in Refinery.Tactic

Methods

hole :: ExceptT err m ext

MonadExtract ext m => MonadExtract ext (StateT s m)

Defined in Refinery.Tactic

Methods

hole :: StateT s m ext

MonadExtract ext m => MonadExtract ext (RuleT jdg ext m)

Defined in Refinery.Tactic

Methods

hole :: RuleT jdg ext m ext

MonadExtract ext m => MonadExtract ext (ReaderT env m)

Defined in Refinery.Tactic

Methods

hole :: ReaderT env m ext

MonadExtract ext m => MonadExtract ext (Proxy a' a b' b m)

Defined in Refinery.Tactic

Methods

hole :: Proxy a' a b' b m ext

class Monad m => MonadRule jdg ext m | m -> jdg, m -> ext where

Minimal complete definition

Nothing

Methods

subgoal :: jdg -> m ext

Create a subgoal, and return the resulting extract.

subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext

Create a subgoal, and return the resulting extract.

Instances

MonadRule jdg ext m => MonadRule jdg ext (ProvableT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ProvableT env m ext

MonadRule jdg ext m => MonadRule jdg ext (ExceptT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ExceptT env m ext

MonadRule jdg ext m => MonadRule jdg ext (StateT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> StateT env m ext

MonadRule jdg ext m => MonadRule jdg ext (ReaderT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ReaderT env m ext

Monad m => MonadRule jdg ext (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> RuleT jdg ext m ext

data RuleT jdg ext m a

A RuleT is a monad transformer for creating inference rules.

Instances

Monad m => MonadRule jdg ext (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> RuleT jdg ext m ext

MonadState s m => MonadState s (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

get :: RuleT jdg ext m s

put :: s -> RuleT jdg ext m ()

state :: (s -> (a, s)) -> RuleT jdg ext m a

MonadReader env m => MonadReader env (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

ask :: RuleT jdg ext m env

local :: (env -> env) -> RuleT jdg ext m a -> RuleT jdg ext m a

reader :: (env -> a) -> RuleT jdg ext m a

MonadError err m => MonadError err (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

throwError :: err -> RuleT jdg ext m a

catchError :: RuleT jdg ext m a -> (err -> RuleT jdg ext m a) -> RuleT jdg ext m a

MonadExtract ext m => MonadExtract ext (RuleT jdg ext m)

Defined in Refinery.Tactic

Methods

hole :: RuleT jdg ext m ext

MFunctor (RuleT jdg ext :: (Type -> Type) -> Type -> Type)

Defined in Refinery.Tactic.Internal

Methods

hoist :: Monad m => (forall a. m a -> n a) -> RuleT jdg ext m b -> RuleT jdg ext n b

MonadTrans (RuleT jdg ext)

Defined in Refinery.Tactic.Internal

Methods

lift :: Monad m => m a -> RuleT jdg ext m a

Functor m => Monad (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: RuleT jdg ext m a -> (a -> RuleT jdg ext m b) -> RuleT jdg ext m b

(>>) :: RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m b

return :: a -> RuleT jdg ext m a

fail :: String -> RuleT jdg ext m a

Functor m => Functor (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

fmap :: (a -> b) -> RuleT jdg ext m a -> RuleT jdg ext m b

(<$) :: a -> RuleT jdg ext m b -> RuleT jdg ext m a

Functor m => Applicative (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

pure :: a -> RuleT jdg ext m a

(<*>) :: RuleT jdg ext m (a -> b) -> RuleT jdg ext m a -> RuleT jdg ext m b

liftA2 :: (a -> b -> c) -> RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m c

(*>) :: RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m b

(<*) :: RuleT jdg ext m a -> RuleT jdg ext m b -> RuleT jdg ext m a

MonadIO m => MonadIO (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> RuleT jdg ext m a

MonadThrow m => MonadThrow (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

throwM :: Exception e => e -> RuleT jdg ext m a

MonadCatch m => MonadCatch (RuleT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

catch :: Exception e => RuleT jdg ext m a -> (e -> RuleT jdg ext m a) -> RuleT jdg ext m a

rule :: Monad m => (jdg -> RuleT jdg ext m ext) -> TacticT jdg ext m ()

Turn an inference rule into a tactic.

class Monad m => MonadProvable jdg m | m -> jdg where

Minimal complete definition

Nothing

Methods

proving :: jdg -> m jdg

Applies a transformation of goals at every step of the tactic.

proving :: (MonadTrans t, MonadProvable jdg m1, m ~ t m1) => jdg -> m jdg

Applies a transformation of goals at every step of the tactic.

Instances

Monad m => MonadProvable jdg (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProvableT jdg m jdg

MonadProvable jdg m => MonadProvable jdg (ExceptT err m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ExceptT err m jdg

MonadProvable jdg m => MonadProvable jdg (StateT s m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> StateT s m jdg

MonadProvable jdg m => MonadProvable jdg (ProofStateT ext m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProofStateT ext m jdg

MonadProvable jdg m => MonadProvable jdg (ReaderT r m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ReaderT r m jdg

newtype ProvableT jdg m a

Helper newtype for when you don't have any need for the mechanisms of MonadProvable.

Constructors

ProvableT

Fields

• runProvableT :: m a

Instances

MonadRule jdg ext m => MonadRule jdg ext (ProvableT env m)

Defined in Refinery.Tactic.Internal

Methods

subgoal :: jdg -> ProvableT env m ext

MonadState s m => MonadState s (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

get :: ProvableT jdg m s

put :: s -> ProvableT jdg m ()

state :: (s -> (a, s)) -> ProvableT jdg m a

MonadError err m => MonadError err (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

throwError :: err -> ProvableT jdg m a

catchError :: ProvableT jdg m a -> (err -> ProvableT jdg m a) -> ProvableT jdg m a

Monad m => MonadProvable jdg (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProvableT jdg m jdg

MonadTrans (ProvableT jdg)

Defined in Refinery.Tactic.Internal

Methods

lift :: Monad m => m a -> ProvableT jdg m a

Monad m => Monad (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

(>>=) :: ProvableT jdg m a -> (a -> ProvableT jdg m b) -> ProvableT jdg m b

(>>) :: ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m b

return :: a -> ProvableT jdg m a

fail :: String -> ProvableT jdg m a

Functor m => Functor (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

fmap :: (a -> b) -> ProvableT jdg m a -> ProvableT jdg m b

(<$) :: a -> ProvableT jdg m b -> ProvableT jdg m a

Applicative m => Applicative (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

pure :: a -> ProvableT jdg m a

(<*>) :: ProvableT jdg m (a -> b) -> ProvableT jdg m a -> ProvableT jdg m b

liftA2 :: (a -> b -> c) -> ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m c

(*>) :: ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m b

(<*) :: ProvableT jdg m a -> ProvableT jdg m b -> ProvableT jdg m a

MonadIO m => MonadIO (ProvableT jdg m)

Defined in Refinery.Tactic.Internal

Methods

liftIO :: IO a -> ProvableT jdg m a

type Provable jdg a = ProvableT jdg Identity a

runProvable :: Provable jdg a -> a

Re-Exports

class Functor f => Alt (f :: Type -> Type) where

Laws:

<!> is associative:             (a <!> b) <!> c = a <!> (b <!> c)
<$> left-distributes over <!>:  f <$> (a <!> b) = (f <$> a) <!> (f <$> b)

If extended to an Alternative then <!> should equal <|>.

Ideally, an instance of Alt also satisfies the "left distributon" law of MonadPlus with respect to <.>:

<.> right-distributes over <!>: (a <!> b) <.> c = (a <.> c) <!> (b <.> c)

But Maybe, IO, Either a, ErrorT e m, and STM satisfy the alternative "left catch" law instead:

pure a <!> b = pure a

However, this variation cannot be stated purely in terms of the dependencies of Alt.

When and if MonadPlus is successfully refactored, this class should also be refactored to remove these instances.

The right distributive law should extend in the cases where the a Bind or Monad is provided to yield variations of the right distributive law:

(m <!> n) >>- f = (m >>- f) <!> (m >>- f)
(m <!> n) >>= f = (m >>= f) <!> (m >>= f)

Minimal complete definition

(<!>)

Methods

(<!>) :: f a -> f a -> f a infixl 3

<|> without a required empty

some :: Applicative f => f a -> f [a]

many :: Applicative f => f a -> f [a]

Instances

Alt []

Defined in Data.Functor.Alt

Methods

(<!>) :: [a] -> [a] -> [a]

some :: Applicative [] => [a] -> [[a]]

many :: Applicative [] => [a] -> [[a]]

Alt Maybe

Defined in Data.Functor.Alt

Methods

(<!>) :: Maybe a -> Maybe a -> Maybe a

some :: Applicative Maybe => Maybe a -> Maybe [a]

many :: Applicative Maybe => Maybe a -> Maybe [a]

Alt IO

This instance does not actually satisfy the (<.>) right distributive law It instead satisfies the "Left-Catch" law

Defined in Data.Functor.Alt

Methods

(<!>) :: IO a -> IO a -> IO a

some :: Applicative IO => IO a -> IO [a]

many :: Applicative IO => IO a -> IO [a]

Alt First

Defined in Data.Functor.Alt

Methods

(<!>) :: First a -> First a -> First a

some :: Applicative First => First a -> First [a]

many :: Applicative First => First a -> First [a]

Alt Last

Defined in Data.Functor.Alt

Methods

(<!>) :: Last a -> Last a -> Last a

some :: Applicative Last => Last a -> Last [a]

many :: Applicative Last => Last a -> Last [a]

Alt Option

Defined in Data.Functor.Alt

Methods

(<!>) :: Option a -> Option a -> Option a

some :: Applicative Option => Option a -> Option [a]

many :: Applicative Option => Option a -> Option [a]

Alt First

Defined in Data.Functor.Alt

Methods

(<!>) :: First a -> First a -> First a

some :: Applicative First => First a -> First [a]

many :: Applicative First => First a -> First [a]

Alt Last

Defined in Data.Functor.Alt

Methods

(<!>) :: Last a -> Last a -> Last a

some :: Applicative Last => Last a -> Last [a]

many :: Applicative Last => Last a -> Last [a]

Alt NonEmpty

Defined in Data.Functor.Alt

Methods

(<!>) :: NonEmpty a -> NonEmpty a -> NonEmpty a

some :: Applicative NonEmpty => NonEmpty a -> NonEmpty [a]

many :: Applicative NonEmpty => NonEmpty a -> NonEmpty [a]

Alt IntMap

Defined in Data.Functor.Alt

Methods

(<!>) :: IntMap a -> IntMap a -> IntMap a

some :: Applicative IntMap => IntMap a -> IntMap [a]

many :: Applicative IntMap => IntMap a -> IntMap [a]

Alt Seq

Defined in Data.Functor.Alt

Methods

(<!>) :: Seq a -> Seq a -> Seq a

some :: Applicative Seq => Seq a -> Seq [a]

many :: Applicative Seq => Seq a -> Seq [a]

Alt (Either a)

Defined in Data.Functor.Alt

Methods

(<!>) :: Either a a0 -> Either a a0 -> Either a a0

some :: Applicative (Either a) => Either a a0 -> Either a [a0]

many :: Applicative (Either a) => Either a a0 -> Either a [a0]

Alt (V1 :: Type -> Type)

Defined in Data.Functor.Alt

Methods

(<!>) :: V1 a -> V1 a -> V1 a

some :: Applicative V1 => V1 a -> V1 [a]

many :: Applicative V1 => V1 a -> V1 [a]

Alt (U1 :: Type -> Type)

Defined in Data.Functor.Alt

Methods

(<!>) :: U1 a -> U1 a -> U1 a

some :: Applicative U1 => U1 a -> U1 [a]

many :: Applicative U1 => U1 a -> U1 [a]

MonadPlus m => Alt (WrappedMonad m)

Defined in Data.Functor.Alt

Methods

(<!>) :: WrappedMonad m a -> WrappedMonad m a -> WrappedMonad m a

some :: Applicative (WrappedMonad m) => WrappedMonad m a -> WrappedMonad m [a]

many :: Applicative (WrappedMonad m) => WrappedMonad m a -> WrappedMonad m [a]

Alt (Proxy :: Type -> Type)

Defined in Data.Functor.Alt

Methods

(<!>) :: Proxy a -> Proxy a -> Proxy a

some :: Applicative Proxy => Proxy a -> Proxy [a]

many :: Applicative Proxy => Proxy a -> Proxy [a]

Ord k => Alt (Map k)

Defined in Data.Functor.Alt

Methods

(<!>) :: Map k a -> Map k a -> Map k a

some :: Applicative (Map k) => Map k a -> Map k [a]

many :: Applicative (Map k) => Map k a -> Map k [a]

(Bind f, Monad f) => Alt (MaybeT f)

Defined in Data.Functor.Alt

Methods

(<!>) :: MaybeT f a -> MaybeT f a -> MaybeT f a

some :: Applicative (MaybeT f) => MaybeT f a -> MaybeT f [a]

many :: Applicative (MaybeT f) => MaybeT f a -> MaybeT f [a]

Apply f => Alt (ListT f)

Defined in Data.Functor.Alt

Methods

(<!>) :: ListT f a -> ListT f a -> ListT f a

some :: Applicative (ListT f) => ListT f a -> ListT f [a]

many :: Applicative (ListT f) => ListT f a -> ListT f [a]

Alternative f => Alt (WrappedApplicative f)

Defined in Data.Functor.Alt

Methods

(<!>) :: WrappedApplicative f a -> WrappedApplicative f a -> WrappedApplicative f a

some :: Applicative (WrappedApplicative f) => WrappedApplicative f a -> WrappedApplicative f [a]

many :: Applicative (WrappedApplicative f) => WrappedApplicative f a -> WrappedApplicative f [a]

Alt f => Alt (Lift f)

Defined in Data.Functor.Alt

Methods

(<!>) :: Lift f a -> Lift f a -> Lift f a

some :: Applicative (Lift f) => Lift f a -> Lift f [a]

many :: Applicative (Lift f) => Lift f a -> Lift f [a]

Alt f => Alt (Rec1 f)

Defined in Data.Functor.Alt

Methods

(<!>) :: Rec1 f a -> Rec1 f a -> Rec1 f a

some :: Applicative (Rec1 f) => Rec1 f a -> Rec1 f [a]

many :: Applicative (Rec1 f) => Rec1 f a -> Rec1 f [a]

ArrowPlus a => Alt (WrappedArrow a b)

Defined in Data.Functor.Alt

Methods

(<!>) :: WrappedArrow a b a0 -> WrappedArrow a b a0 -> WrappedArrow a b a0

some :: Applicative (WrappedArrow a b) => WrappedArrow a b a0 -> WrappedArrow a b [a0]

many :: Applicative (WrappedArrow a b) => WrappedArrow a b a0 -> WrappedArrow a b [a0]

Alt f => Alt (IdentityT f)

Defined in Data.Functor.Alt

Methods

(<!>) :: IdentityT f a -> IdentityT f a -> IdentityT f a

some :: Applicative (IdentityT f) => IdentityT f a -> IdentityT f [a]

many :: Applicative (IdentityT f) => IdentityT f a -> IdentityT f [a]

(Bind f, Monad f, Semigroup e) => Alt (ExceptT e f)

Defined in Data.Functor.Alt

Methods

(<!>) :: ExceptT e f a -> ExceptT e f a -> ExceptT e f a

some :: Applicative (ExceptT e f) => ExceptT e f a -> ExceptT e f [a]

many :: Applicative (ExceptT e f) => ExceptT e f a -> ExceptT e f [a]

(Bind f, Monad f) => Alt (ErrorT e f)

Defined in Data.Functor.Alt

Methods

(<!>) :: ErrorT e f a -> ErrorT e f a -> ErrorT e f a

some :: Applicative (ErrorT e f) => ErrorT e f a -> ErrorT e f [a]

many :: Applicative (ErrorT e f) => ErrorT e f a -> ErrorT e f [a]

Alt f => Alt (StateT e f)

Defined in Data.Functor.Alt

Methods

(<!>) :: StateT e f a -> StateT e f a -> StateT e f a

some :: Applicative (StateT e f) => StateT e f a -> StateT e f [a]

many :: Applicative (StateT e f) => StateT e f a -> StateT e f [a]

Alt f => Alt (StateT e f)

Defined in Data.Functor.Alt

Methods

(<!>) :: StateT e f a -> StateT e f a -> StateT e f a

some :: Applicative (StateT e f) => StateT e f a -> StateT e f [a]

many :: Applicative (StateT e f) => StateT e f a -> StateT e f [a]

Alt f => Alt (WriterT w f)

Defined in Data.Functor.Alt

Methods

(<!>) :: WriterT w f a -> WriterT w f a -> WriterT w f a

some :: Applicative (WriterT w f) => WriterT w f a -> WriterT w f [a]

many :: Applicative (WriterT w f) => WriterT w f a -> WriterT w f [a]

Alt f => Alt (WriterT w f)

Defined in Data.Functor.Alt

Methods

(<!>) :: WriterT w f a -> WriterT w f a -> WriterT w f a

some :: Applicative (WriterT w f) => WriterT w f a -> WriterT w f [a]

many :: Applicative (WriterT w f) => WriterT w f a -> WriterT w f [a]

Alt f => Alt (Reverse f)

Defined in Data.Functor.Alt

Methods

(<!>) :: Reverse f a -> Reverse f a -> Reverse f a

some :: Applicative (Reverse f) => Reverse f a -> Reverse f [a]

many :: Applicative (Reverse f) => Reverse f a -> Reverse f [a]

Alt f => Alt (Backwards f)

Defined in Data.Functor.Alt

Methods

(<!>) :: Backwards f a -> Backwards f a -> Backwards f a

some :: Applicative (Backwards f) => Backwards f a -> Backwards f [a]

many :: Applicative (Backwards f) => Backwards f a -> Backwards f [a]

(Alt f, Alt g) => Alt (f :*: g)

Defined in Data.Functor.Alt

Methods

(<!>) :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a

some :: Applicative (f :*: g) => (f :*: g) a -> (f :*: g) [a]

many :: Applicative (f :*: g) => (f :*: g) a -> (f :*: g) [a]

(Alt f, Alt g) => Alt (Product f g)

Defined in Data.Functor.Alt

Methods

(<!>) :: Product f g a -> Product f g a -> Product f g a

some :: Applicative (Product f g) => Product f g a -> Product f g [a]

many :: Applicative (Product f g) => Product f g a -> Product f g [a]

Alt f => Alt (ReaderT e f)

Defined in Data.Functor.Alt

Methods

(<!>) :: ReaderT e f a -> ReaderT e f a -> ReaderT e f a

some :: Applicative (ReaderT e f) => ReaderT e f a -> ReaderT e f [a]

many :: Applicative (ReaderT e f) => ReaderT e f a -> ReaderT e f [a]

MonadError err m => Alt (TacticT jdg ext m)

Defined in Refinery.Tactic.Internal

Methods

(<!>) :: TacticT jdg ext m a -> TacticT jdg ext m a -> TacticT jdg ext m a

some :: Applicative (TacticT jdg ext m) => TacticT jdg ext m a -> TacticT jdg ext m [a]

many :: Applicative (TacticT jdg ext m) => TacticT jdg ext m a -> TacticT jdg ext m [a]

Alt f => Alt (M1 i c f)

Defined in Data.Functor.Alt

Methods

(<!>) :: M1 i c f a -> M1 i c f a -> M1 i c f a

some :: Applicative (M1 i c f) => M1 i c f a -> M1 i c f [a]

many :: Applicative (M1 i c f) => M1 i c f a -> M1 i c f [a]

(Alt f, Functor g) => Alt (Compose f g)

Defined in Data.Functor.Alt

Methods

(<!>) :: Compose f g a -> Compose f g a -> Compose f g a

some :: Applicative (Compose f g) => Compose f g a -> Compose f g [a]

many :: Applicative (Compose f g) => Compose f g a -> Compose f g [a]

Alt f => Alt (RWST r w s f)

Defined in Data.Functor.Alt

Methods

(<!>) :: RWST r w s f a -> RWST r w s f a -> RWST r w s f a

some :: Applicative (RWST r w s f) => RWST r w s f a -> RWST r w s f [a]

many :: Applicative (RWST r w s f) => RWST r w s f a -> RWST r w s f [a]

Alt f => Alt (RWST r w s f)

Defined in Data.Functor.Alt

Methods

(<!>) :: RWST r w s f a -> RWST r w s f a -> RWST r w s f a

some :: Applicative (RWST r w s f) => RWST r w s f a -> RWST r w s f [a]

many :: Applicative (RWST r w s f) => RWST r w s f a -> RWST r w s f [a]