Safe Haskell	None
Language	Haskell2010

Agda.Utils.Maybe

Description

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.

Synopsis

boolToMaybe :: Bool -> a -> Maybe a
caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b
whenNothing :: Monoid m => Maybe a -> m -> m
fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a
forMaybe :: [a] -> (a -> Maybe b) -> [b]
filterMaybe :: (a -> Bool) -> a -> Maybe a
allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a])
whenNothingM :: Monad m => m (Maybe a) -> m () -> m ()
whenJust :: Monad m => Maybe a -> (a -> m ()) -> m ()
unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionsMaybeWith :: (a -> a -> a) -> [Maybe a] -> Maybe a
unzipMaybe :: Maybe (a, b) -> (Maybe a, Maybe b)
caseMaybe :: Maybe a -> b -> (a -> b) -> b
ifJust :: Maybe a -> (a -> b) -> b -> b
maybeM :: Monad m => m b -> (a -> m b) -> m (Maybe a) -> m b
ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b
whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m ()
liftMaybe :: Alternative f => Maybe a -> f a
spanMaybe :: (a -> Maybe b) -> [a] -> ([b], [a])
data Maybe a
- = Nothing
- | Just a
catMaybes :: [Maybe a] -> [a]
fromMaybe :: a -> Maybe a -> a
listToMaybe :: [a] -> Maybe a
maybeToList :: Maybe a -> [a]
maybe :: b -> (a -> b) -> Maybe a -> b
isNothing :: Maybe a -> Bool
mapMaybe :: (a -> Maybe b) -> [a] -> [b]
fromJust :: HasCallStack => Maybe a -> a
isJust :: Maybe a -> Bool

Documentation

boolToMaybe :: Bool -> a -> Maybe a Source #

Retain object when tag is True.

caseMaybeM :: Monad m => m (Maybe a) -> m b -> (a -> m b) -> m b Source #

Monadic version of caseMaybe. That is, maybeM with a different argument ordering.

whenNothing :: Monoid m => Maybe a -> m -> m Source #

caseMaybe without the Just case.

fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a Source #

Monadic version of fromMaybe.

forMaybe :: [a] -> (a -> Maybe b) -> [b] Source #

Version of mapMaybe with different argument ordering.

filterMaybe :: (a -> Bool) -> a -> Maybe a Source #

Filtering a singleton list.

filterMaybe p a = listToMaybe (filter p [a])

allJustM :: Monad m => [m (Maybe a)] -> m (Maybe [a]) Source #

Lazy version of allJust . sequence. (allJust = mapM for the Maybe monad.) Only executes monadic effect while isJust.

whenNothingM :: Monad m => m (Maybe a) -> m () -> m () Source #

caseMaybeM without the Just case.

whenJust :: Monad m => Maybe a -> (a -> m ()) -> m () Source #

A more telling name for forM_ for the Maybe collection type. Or: caseMaybe without the Nothing case.

unionMaybeWith :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a Source #

unionWith for collections of size <= 1.

unionsMaybeWith :: (a -> a -> a) -> [Maybe a] -> Maybe a Source #

unionsWith for collections of size <= 1.

unzipMaybe :: Maybe (a, b) -> (Maybe a, Maybe b) Source #

Unzipping a list of length <= 1.

caseMaybe :: Maybe a -> b -> (a -> b) -> b Source #

Version of maybe with different argument ordering. Often, we want to case on a Maybe, do something interesting in the Just case, but only a default action in the Nothing case. Then, the argument ordering of caseMaybe is preferable.

caseMaybe m d f = flip (maybe d) m f

ifJust :: Maybe a -> (a -> b) -> b -> b Source #

caseMaybe with flipped branches.

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

Monadic version of maybe.

ifJustM :: Monad m => m (Maybe a) -> (a -> m b) -> m b -> m b Source #

caseMaybeM with flipped branches.

whenJustM :: Monad m => m (Maybe a) -> (a -> m ()) -> m () Source #

caseMaybeM without the Nothing case.

liftMaybe :: Alternative f => Maybe a -> f a Source #

Lift a maybe to an Alternative.

spanMaybe :: (a -> Maybe b) -> [a] -> ([b], [a]) Source #

Like span, takes the prefix of a list satisfying a predicate. Returns the run of Justs until the first Nothing, and the tail of the list.

data Maybe a #

Constructors

Nothing
Just a

Instances

Instances details

Updater1 Maybe Source #

Instance details

Defined in Agda.Utils.Update

Methods

updater1 :: Updater a -> Updater (Maybe a) Source #

updates1 :: Updater a -> Updater (Maybe a) Source #

update1 :: Updater a -> EndoFun (Maybe a) Source #

MonadZip Maybe

Instance details

Defined in Control.Monad.Zip

Methods

mzip :: Maybe a -> Maybe b -> Maybe (a, b)

mzipWith :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c

munzip :: Maybe (a, b) -> (Maybe a, Maybe b)

Eq1 Maybe

Instance details

Defined in Data.Functor.Classes

Methods

liftEq :: (a -> b -> Bool) -> Maybe a -> Maybe b -> Bool

Ord1 Maybe

Instance details

Defined in Data.Functor.Classes

Methods

liftCompare :: (a -> b -> Ordering) -> Maybe a -> Maybe b -> Ordering

Read1 Maybe

Instance details

Defined in Data.Functor.Classes

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Maybe a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Maybe a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Maybe a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Maybe a]

Show1 Maybe

Instance details

Defined in Data.Functor.Classes

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Maybe a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Maybe a] -> ShowS

NFData1 Maybe

Instance details

Defined in Control.DeepSeq

Methods

liftRnf :: (a -> ()) -> Maybe a -> ()

MonadThrow Maybe

Instance details

Defined in Control.Monad.Catch

Methods

throwM :: (HasCallStack, Exception e) => e -> Maybe a

Alternative Maybe

Instance details

Defined in GHC.Internal.Base

Methods

empty :: Maybe a

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

some :: Maybe a -> Maybe [a]

many :: Maybe a -> Maybe [a]

Applicative Maybe

Instance details

Defined in GHC.Internal.Base

Methods

pure :: a -> Maybe a

(<*>) :: Maybe (a -> b) -> Maybe a -> Maybe b #

liftA2 :: (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c

(*>) :: Maybe a -> Maybe b -> Maybe b

(<*) :: Maybe a -> Maybe b -> Maybe a

Functor Maybe

Instance details

Defined in GHC.Internal.Base

Methods

fmap :: (a -> b) -> Maybe a -> Maybe b

(<$) :: a -> Maybe b -> Maybe a #

Monad Maybe

Instance details

Defined in GHC.Internal.Base

Methods

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b

(>>) :: Maybe a -> Maybe b -> Maybe b

return :: a -> Maybe a

MonadPlus Maybe

Instance details

Defined in GHC.Internal.Base

Methods

mzero :: Maybe a #

mplus :: Maybe a -> Maybe a -> Maybe a #

MonadFail Maybe

Instance details

Defined in GHC.Internal.Control.Monad.Fail

Methods

fail :: String -> Maybe a

MonadFix Maybe

Instance details

Defined in GHC.Internal.Control.Monad.Fix

Methods

mfix :: (a -> Maybe a) -> Maybe a

Foldable Maybe

Instance details

Defined in GHC.Internal.Data.Foldable

Methods

fold :: Monoid m => Maybe m -> m

foldMap :: Monoid m => (a -> m) -> Maybe a -> m

foldMap' :: Monoid m => (a -> m) -> Maybe a -> m

foldr :: (a -> b -> b) -> b -> Maybe a -> b

foldr' :: (a -> b -> b) -> b -> Maybe a -> b

foldl :: (b -> a -> b) -> b -> Maybe a -> b

foldl' :: (b -> a -> b) -> b -> Maybe a -> b

foldr1 :: (a -> a -> a) -> Maybe a -> a

foldl1 :: (a -> a -> a) -> Maybe a -> a

toList :: Maybe a -> [a]

null :: Maybe a -> Bool

length :: Maybe a -> Int

elem :: Eq a => a -> Maybe a -> Bool

maximum :: Ord a => Maybe a -> a

minimum :: Ord a => Maybe a -> a

sum :: Num a => Maybe a -> a

product :: Num a => Maybe a -> a

Traversable Maybe

Instance details

Defined in GHC.Internal.Data.Traversable

Methods

traverse :: Applicative f => (a -> f b) -> Maybe a -> f (Maybe b)

sequenceA :: Applicative f => Maybe (f a) -> f (Maybe a)

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

sequence :: Monad m => Maybe (m a) -> m (Maybe a)

Hashable1 Maybe

Instance details

Defined in Data.Hashable.Class

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> Maybe a -> Int

FromJSON1 Maybe

Instance details

Defined in Data.Aeson.Types.FromJSON

Methods

liftParseJSON :: Maybe a -> (Value -> Parser a) -> (Value -> Parser [a]) -> Value -> Parser (Maybe a) #

liftParseJSONList :: Maybe a -> (Value -> Parser a) -> (Value -> Parser [a]) -> Value -> Parser [Maybe a] #

liftOmittedField :: Maybe a -> Maybe (Maybe a) #

ToJSON1 Maybe

Instance details

Defined in Data.Aeson.Types.ToJSON

Methods

liftToJSON :: (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> Maybe a -> Value #

liftToJSONList :: (a -> Bool) -> (a -> Value) -> ([a] -> Value) -> [Maybe a] -> Value #

liftToEncoding :: (a -> Bool) -> (a -> Encoding) -> ([a] -> Encoding) -> Maybe a -> Encoding #

liftToEncodingList :: (a -> Bool) -> (a -> Encoding) -> ([a] -> Encoding) -> [Maybe a] -> Encoding #

liftOmitField :: (a -> Bool) -> Maybe a -> Bool #

Generic1 Maybe

Instance details

Defined in GHC.Internal.Generics

Associated Types

type Rep1 Maybe
Instance details Defined in GHC.Internal.Generics type Rep1 Maybe = D1 ('MetaData "Maybe" "GHC.Internal.Maybe" "ghc-internal" 'False) (C1 ('MetaCons "Nothing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Just" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

Methods

from1 :: Maybe a -> Rep1 Maybe a

to1 :: Rep1 Maybe a -> Maybe a

MonadBaseControl Maybe Maybe

Instance details

Defined in Control.Monad.Trans.Control

Associated Types

type StM Maybe a
Instance details Defined in Control.Monad.Trans.Control type StM Maybe a = a

Methods

liftBaseWith :: (RunInBase Maybe Maybe -> Maybe a) -> Maybe a

restoreM :: StM Maybe a -> Maybe a

MonadError () Maybe

Instance details

Defined in Control.Monad.Error.Class

Methods

throwError :: () -> Maybe a

catchError :: Maybe a -> (() -> Maybe a) -> Maybe a

CMaybe a (Maybe a) Source #

Instance details

Defined in Agda.Utils.Singleton

Methods

cMaybe :: Maybe a -> Maybe a Source #

Singleton a (Maybe a) Source #

Instance details

Defined in Agda.Utils.Singleton

Methods

singleton :: a -> Maybe a Source #

Lift a => Lift (Maybe a :: Type)

Instance details

Defined in Language.Haskell.TH.Syntax

Methods

lift :: Quote m => Maybe a -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Maybe a -> Code m (Maybe a)

Pretty a => Pretty (Maybe a) Source #

Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Maybe a -> Doc Source #

Globals a => Globals (Maybe a) Source #

Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Maybe a -> Set GlobalId Source #

MakeStrict a => MakeStrict (Maybe a) Source #

Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Maybe a -> Maybe a Source #

EncodeTCM a => EncodeTCM (Maybe a) Source #

Instance details

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Maybe a -> TCM Value Source #

SubstExpr a => SubstExpr (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

substExpr :: [(Name, Expr)] -> Maybe a -> Maybe a Source #

APatternLike a => APatternLike (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Associated Types

type ADotT (Maybe a)
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Maybe a) = ADotT a

Methods

foldrAPattern :: Monoid m => (Pattern' (ADotT (Maybe a)) -> m -> m) -> Maybe a -> m Source #

traverseAPatternM :: Monad m => (Pattern' (ADotT (Maybe a)) -> m (Pattern' (ADotT (Maybe a)))) -> (Pattern' (ADotT (Maybe a)) -> m (Pattern' (ADotT (Maybe a)))) -> Maybe a -> m (Maybe a) Source #

MapNamedArgPattern a => MapNamedArgPattern (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Abstract.Pattern

Methods

mapNamedArgPattern :: (NAP -> NAP) -> Maybe a -> Maybe a Source #

DeclaredNames a => DeclaredNames (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

declaredNames :: Collection KName m => Maybe a -> m Source #

ExprLike a => ExprLike (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Abstract.Views

Methods

recurseExpr :: RecurseExprFn m (Maybe a) Source #

foldExpr :: FoldExprFn m (Maybe a) Source #

traverseExpr :: TraverseExprFn m (Maybe a) Source #

mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe a Source #

AllAreOpaque a => AllAreOpaque (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Common

Methods

jointOpacity :: Maybe a -> JointOpacity Source #

AnyIsAbstract a => AnyIsAbstract (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Common

Methods

anyIsAbstract :: Maybe a -> IsAbstract Source #

LensNamed (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Common

Associated Types

type NameOf (Maybe a)
Instance details Defined in Agda.Syntax.Common type NameOf (Maybe a) = a

Methods

lensNamed :: Lens' (Maybe a) (Maybe (NameOf (Maybe a))) Source #

Pretty a => Pretty (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Maybe a -> Doc Source #

prettyPrec :: Int -> Maybe a -> Doc Source #

prettyList :: [Maybe a] -> Doc Source #

ExprLike a => ExprLike (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Concrete.Generic

Methods

mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe a Source #

foldExpr :: Monoid m => (Expr -> m) -> Maybe a -> m Source #

traverseExpr :: Monad m => (Expr -> m Expr) -> Maybe a -> m (Maybe a) Source #

CPatternLike p => CPatternLike (Maybe p) Source #

Instance details

Defined in Agda.Syntax.Concrete.Pattern

Methods

foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Maybe p -> m Source #

traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Maybe p -> m (Maybe p) Source #

traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Maybe p -> m (Maybe p) Source #

GetDefs a => GetDefs (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Maybe a -> m () Source #

TermLike a => TermLike (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Maybe a -> m (Maybe a) Source #

foldTerm :: Monoid m => (Term -> m) -> Maybe a -> m Source #

AllMetas a => AllMetas (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Maybe a -> m Source #

NamesIn a => NamesIn (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Maybe a -> m Source #

HasRange a => HasRange (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Position

Methods

getRange :: Maybe a -> Range Source #

KillRange a => KillRange (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Position

Methods

killRange :: KillRangeT (Maybe a) Source #

SetRange a => SetRange (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Position

Methods

setRange :: Range -> Maybe a -> Maybe a Source #

ToConcrete a => ToConcrete (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe a)
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe a) = Maybe (ConOfAbs a)

Methods

toConcrete :: Maybe a -> AbsToCon (ConOfAbs (Maybe a)) Source #

bindToConcrete :: Maybe a -> (ConOfAbs (Maybe a) -> AbsToCon b) -> AbsToCon b Source #

ToAbstract c => ToAbstract (Maybe c) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Maybe c)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Maybe c) = Maybe (AbsOfCon c)

Methods

toAbstract :: Maybe c -> ScopeM (AbsOfCon (Maybe c)) Source #

AbsTerm a => AbsTerm (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Maybe a -> Maybe a Source #

DropArgs a => DropArgs (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Maybe a -> Maybe a Source #

Free t => Free (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Maybe t -> FreeM a c Source #

PrecomputeFreeVars a => PrecomputeFreeVars (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Maybe a -> FV (Maybe a) Source #

MentionsMeta t => MentionsMeta (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Maybe t -> Bool Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Maybe a -> m Bool Source #

ExpandPatternSynonyms a => ExpandPatternSynonyms (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Patterns.Abstract

Methods

expandPatternSynonyms :: Maybe a -> TCM (Maybe a) Source #

ComputeOccurrences a => ComputeOccurrences (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Positivity

Methods

occurrences :: Maybe a -> OccM OccurrencesBuilder Source #

PrettyTCM a => PrettyTCM (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Maybe a -> m Doc Source #

FromTerm a => FromTerm (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction (Maybe a)) Source #

PrimTerm a => PrimTerm (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Maybe a -> TCM Term Source #

PrimTerm a => PrimType (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primType :: Maybe a -> TCM Type Source #

ToTerm a => ToTerm (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Maybe a -> Term) Source #

toTermR :: TCM (Maybe a -> ReduceM Term) Source #

Instantiate t => Instantiate (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Maybe t -> ReduceM (Maybe t) Source #

InstantiateFull t => InstantiateFull (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Maybe t -> ReduceM (Maybe t) Source #

Normalise t => Normalise (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Maybe t -> ReduceM (Maybe t) Source #

Reduce t => Reduce (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Maybe t -> ReduceM (Maybe t) Source #

reduceB' :: Maybe t -> ReduceM (Blocked (Maybe t)) Source #

Simplify t => Simplify (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Maybe t -> ReduceM (Maybe t)

ChooseFlex a => ChooseFlex (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Maybe a -> Maybe a -> FlexChoice Source #

EmbPrj a => EmbPrj (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Maybe a -> S Int32 Source #

icod_ :: Maybe a -> S Int32 Source #

value :: Int32 -> R (Maybe a) Source #

Abstract t => Abstract (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Maybe t -> Maybe t Source #

Apply t => Apply (Maybe t) Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Maybe t -> Args -> Maybe t Source #

applyE :: Maybe t -> Elims -> Maybe t Source #

Subst a => Subst (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Maybe a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Maybe a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a Source #

Null (Maybe a) Source #

A Maybe is null when it corresponds to the empty list.

Instance details

Defined in Agda.Utils.Null

Methods

empty :: Maybe a Source #

null :: Maybe a -> Bool Source #

PartialOrd a => PartialOrd (Maybe a) Source #

Nothing and Just _ are unrelated.

Partial ordering for Maybe a is the same as for Either () a.

Instance details

Defined in Agda.Utils.PartialOrd

Methods

comparable :: Comparable (Maybe a) Source #

SemiRing a => SemiRing (Maybe a) Source #

Instance details

Defined in Agda.Utils.SemiRing

Methods

ozero :: Maybe a Source #

oone :: Maybe a Source #

oplus :: Maybe a -> Maybe a -> Maybe a Source #

otimes :: Maybe a -> Maybe a -> Maybe a Source #

StarSemiRing a => StarSemiRing (Maybe a) Source #

Instance details

Defined in Agda.Utils.SemiRing

Methods

ostar :: Maybe a -> Maybe a Source #

Binary a => Binary (Maybe a)

Instance details

Defined in Data.Binary.Class

Methods

put :: Maybe a -> Put

get :: Get (Maybe a)

putList :: [Maybe a] -> Put

NFData a => NFData (Maybe a)

Instance details

Defined in Control.DeepSeq

Methods

rnf :: Maybe a -> ()

Hashable a => Hashable (Maybe a)

Instance details

Defined in Data.Hash.Instances

Methods

hash :: Maybe a -> Hash

Semigroup a => Monoid (Maybe a)

Instance details

Defined in GHC.Internal.Base

Methods

mempty :: Maybe a

mappend :: Maybe a -> Maybe a -> Maybe a

mconcat :: [Maybe a] -> Maybe a

Semigroup a => Semigroup (Maybe a)

Instance details

Defined in GHC.Internal.Base

Methods

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

sconcat :: NonEmpty (Maybe a) -> Maybe a

stimes :: Integral b => b -> Maybe a -> Maybe a

Generic (Maybe a)

Instance details

Defined in GHC.Internal.Generics

Associated Types

type Rep (Maybe a)
Instance details Defined in GHC.Internal.Generics type Rep (Maybe a) = D1 ('MetaData "Maybe" "GHC.Internal.Maybe" "ghc-internal" 'False) (C1 ('MetaCons "Nothing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Just" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

from :: Maybe a -> Rep (Maybe a) x

to :: Rep (Maybe a) x -> Maybe a

SingKind a => SingKind (Maybe a)

Instance details

Defined in GHC.Internal.Generics

Associated Types

type DemoteRep (Maybe a)
Instance details Defined in GHC.Internal.Generics type DemoteRep (Maybe a) = Maybe (DemoteRep a)

Methods

fromSing :: forall (a0 :: Maybe a). Sing a0 -> DemoteRep (Maybe a)

Read a => Read (Maybe a)

Instance details

Defined in GHC.Internal.Read

Methods

readsPrec :: Int -> ReadS (Maybe a)

readList :: ReadS [Maybe a]

readPrec :: ReadPrec (Maybe a)

readListPrec :: ReadPrec [Maybe a]

Show a => Show (Maybe a)

Instance details

Defined in GHC.Internal.Show

Methods

showsPrec :: Int -> Maybe a -> ShowS

show :: Maybe a -> String

showList :: [Maybe a] -> ShowS

Eq a => Eq (Maybe a)

Instance details

Defined in GHC.Internal.Maybe

Methods

(==) :: Maybe a -> Maybe a -> Bool

(/=) :: Maybe a -> Maybe a -> Bool

Ord a => Ord (Maybe a)

Instance details

Defined in GHC.Internal.Maybe

Methods

compare :: Maybe a -> Maybe a -> Ordering

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

(<=) :: Maybe a -> Maybe a -> Bool

(>) :: Maybe a -> Maybe a -> Bool

(>=) :: Maybe a -> Maybe a -> Bool

max :: Maybe a -> Maybe a -> Maybe a

min :: Maybe a -> Maybe a -> Maybe a

Hashable a => Hashable (Maybe a)

Instance details

Defined in Data.Hashable.Class

Methods

hashWithSalt :: Int -> Maybe a -> Int

hash :: Maybe a -> Int

Hashable32 a => Hashable32 (Maybe a)

Instance details

Defined in Data.Digest.Murmur32

Methods

hash32Add :: Maybe a -> Hash32 -> Hash32

Hashable64 a => Hashable64 (Maybe a)

Instance details

Defined in Data.Digest.Murmur64

Methods

hash64Add :: Maybe a -> Hash64 -> Hash64

Pretty a => Pretty (Maybe a)

Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJClass

Methods

pPrintPrec :: PrettyLevel -> Rational -> Maybe a -> Doc ann

pPrint :: Maybe a -> Doc ann

pPrintList :: PrettyLevel -> [Maybe a] -> Doc ann

Pretty a => Pretty (Maybe a)

Instance details

Defined in Text.PrettyPrint.HughesPJClass

Methods

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

pPrint :: Maybe a -> Doc

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

FromJSON a => FromJSON (Maybe a)

Instance details

Defined in Data.Aeson.Types.FromJSON

Methods

parseJSON :: Value -> Parser (Maybe a) #

parseJSONList :: Value -> Parser [Maybe a] #

omittedField :: Maybe (Maybe a) #

ToJSON a => ToJSON (Maybe a)

Instance details

Defined in Data.Aeson.Types.ToJSON

Methods

toJSON :: Maybe a -> Value #

toEncoding :: Maybe a -> Encoding #

toJSONList :: [Maybe a] -> Value #

toEncodingList :: [Maybe a] -> Encoding #

omitField :: Maybe a -> Bool #

InversePermute [Maybe a] (IntMap a) Source #

Instance details

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> [Maybe a] -> IntMap a Source #

InversePermute [Maybe a] [Maybe a] Source #

Instance details

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> [Maybe a] -> [Maybe a] Source #

InversePermute [Maybe a] [(Int, a)] Source #

Instance details

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> [Maybe a] -> [(Int, a)] Source #

SingI ('Nothing :: Maybe a)

Instance details

Defined in GHC.Internal.Generics

Methods

sing :: Sing ('Nothing :: Maybe a)

Strict (Maybe a) (Maybe a)

Instance details

Defined in Data.Strict.Classes

Methods

toStrict :: Maybe a -> Maybe a #

toLazy :: Maybe a -> Maybe a #

SingI a2 => SingI ('Just a2 :: Maybe a1)

Instance details

Defined in GHC.Internal.Generics

Methods

sing :: Sing ('Just a2)

InversePermute (Int -> a) [Maybe a] Source #

Instance details

Defined in Agda.Utils.Permutation

Methods

inversePermute :: Permutation -> (Int -> a) -> [Maybe a] Source #

type Rep1 Maybe

Instance details

Defined in GHC.Internal.Generics

type Rep1 Maybe = D1 ('MetaData "Maybe" "GHC.Internal.Maybe" "ghc-internal" 'False) (C1 ('MetaCons "Nothing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Just" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

type StM Maybe a

Instance details

Defined in Control.Monad.Trans.Control

type StM Maybe a = a

type ADotT (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Abstract.Pattern

type ADotT (Maybe a) = ADotT a

type NameOf (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Common

type NameOf (Maybe a) = a

type ConOfAbs (Maybe a) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe a) = Maybe (ConOfAbs a)

type AbsOfCon (Maybe c) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Maybe c) = Maybe (AbsOfCon c)

type SubstArg (Maybe a) Source #

Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Maybe a) = SubstArg a

type DemoteRep (Maybe a)

Instance details

Defined in GHC.Internal.Generics

type DemoteRep (Maybe a) = Maybe (DemoteRep a)

type Rep (Maybe a)

Instance details

Defined in GHC.Internal.Generics

type Rep (Maybe a) = D1 ('MetaData "Maybe" "GHC.Internal.Maybe" "ghc-internal" 'False) (C1 ('MetaCons "Nothing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Just" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data Sing (b :: Maybe a)

Instance details

Defined in GHC.Internal.Generics

data Sing (b :: Maybe a) where

SNothing :: forall {a}. Sing ('Nothing :: Maybe a)
SJust :: forall {a} (a1 :: a). Sing a1 -> Sing ('Just a1)

catMaybes :: [Maybe a] -> [a] #

fromMaybe :: a -> Maybe a -> a #

listToMaybe :: [a] -> Maybe a #

maybeToList :: Maybe a -> [a] #

maybe :: b -> (a -> b) -> Maybe a -> b #

isNothing :: Maybe a -> Bool #

mapMaybe :: (a -> Maybe b) -> [a] -> [b] #

fromJust :: HasCallStack => Maybe a -> a #

isJust :: Maybe a -> Bool #