Maybe package:Agda

Extend Maybe by common operations for the Maybe type. Note: since this module is usually imported unqualified, we do not use short names, but all names contain Maybe, Just, or 'Nothing.

MaybeProjection :: ProjectionLikenessMissing

Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base

Projection-likeness analysis has not run on this function yet. It may do so in the future.

MaybeRed :: IsReduced -> a -> MaybeReduced a

Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base

data MaybeReduced a

Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base

type MaybeReducedElims = [MaybeReduced Elim]

Agda Agda.Compiler.Backend Agda.TypeChecking.Monad.Base

data MaybePlaceholder e

Agda Agda.Syntax.Common

Placeholders are used to represent the underscores in a section.

MaybeFree :: MetaSet -> IsFree

Agda Agda.TypeChecking.Free.Reduce

maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))

Agda Agda.Interaction.InteractionTop

If the next command from the command queue is anything but an actual command, then the command is returned. If the command is an IOTCM command, then the following happens: The given computation is applied to the command and executed. If an abort command is encountered (and acted upon), then the computation is interrupted, the persistent state and all options are restored, and some commands are sent to the frontend. If the computation was not interrupted, then its result is returned.

maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)

Agda Agda.Interaction.InteractionTop

maybeProjTurnPostfix :: Expr -> Maybe Expr

Agda Agda.Syntax.Abstract.Views

maybePlaceholder :: Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)

Agda Agda.Syntax.Concrete.Operators.Parser

maybeNamed :: Expr -> Parser (Named_ Expr)

Agda Agda.Syntax.Parser.Helpers

When given expression is e1 = e2, turn it into a named expression. Call this inside an implicit argument {e} or {{e}}, where an equality must be a named argument (rather than a cubical partial match).

maybePrimCon :: TCM Term -> TCM (Maybe ConHead)

Agda Agda.TypeChecking.Level

maybePrimDef :: TCM Term -> TCM (Maybe QName)

Agda Agda.TypeChecking.Level

maybeFlexiblePattern :: (IsFlexiblePattern a, HasConstInfo m, MonadDebug m) => a -> MaybeT m FlexibleVarKind

Agda Agda.TypeChecking.Rules.LHS

maybeLeft :: Either a b -> Maybe a

Agda Agda.Utils.Either

Safe projection from Left.

maybeLeft (Left a) = Just a
maybeLeft Right{}  = Nothing

maybeRight :: Either a b -> Maybe b

Agda Agda.Utils.Either

Safe projection from Right.

maybeRight (Right b) = Just b
maybeRight Left{}    = Nothing

maybeToEither :: e -> Maybe a -> Either e a

Agda Agda.Utils.Either

Convert Maybe to Either e, given an error e for the Nothing case.

maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b

Agda Agda.Utils.Maybe Agda.Utils.Maybe.Strict

Monadic version of maybe.

BuiltinMaybe :: BuiltinId

Agda Agda.Compiler.Backend

PragmaCompileMaybe :: Warning

Agda Agda.Compiler.Backend

COMPILE GHC pragma for MAYBE; ignored.

RewriteMaybeNonConfluent :: Term -> Term -> [Doc] -> Warning

Agda Agda.Compiler.Backend

Confluence checker got stuck on computing overlap between two rewrite rules

builtinMaybe :: BuiltinId

Agda Agda.Compiler.Backend

primMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

Agda Agda.Compiler.Backend