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]
mapMaybe :: (a -> Maybe b) -> [a] -> [b]
fromMaybe :: a -> Maybe a -> a
listToMaybe :: [a] -> Maybe a
maybeToList :: Maybe a -> [a]
maybe :: b -> (a -> b) -> Maybe a -> b
isNothing :: Maybe a -> Bool
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 #

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 #

MonadFail Maybe

Instance details

Defined in Control.Monad.Fail

Methods

fail :: String -> Maybe a

MonadFix Maybe

Instance details

Defined in Control.Monad.Fix

Methods

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

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)

Foldable Maybe

Instance details

Defined in 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

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

Traversable Maybe

Instance details

Defined in 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)

Alternative Maybe

Instance details

Defined in GHC.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.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.Base

Methods

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

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

Monad Maybe

Instance details

Defined in GHC.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.Base

Methods

mzero :: Maybe a #

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

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

Hashable1 Maybe

Instance details

Defined in Data.Hashable.Class

Methods

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

Generic1 Maybe

Instance details

Defined in GHC.Generics

Associated Types

type Rep1 Maybe
Instance details Defined in GHC.Generics type Rep1 Maybe = D1 ('MetaData "Maybe" "GHC.Maybe" "base" '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

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Term (MExp O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Type (MExp O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

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)

Property BidiPairedBracketType_ (Maybe BidiPairedBracketType)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: BidiPairedBracketType_ -> Int32 -> Maybe BidiPairedBracketType

toUProperty :: BidiPairedBracketType_ -> UProperty

Property Decomposition_ (Maybe Decomposition)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: Decomposition_ -> Int32 -> Maybe Decomposition

toUProperty :: Decomposition_ -> UProperty

Property GraphemeClusterBreak_ (Maybe GraphemeClusterBreak)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: GraphemeClusterBreak_ -> Int32 -> Maybe GraphemeClusterBreak

toUProperty :: GraphemeClusterBreak_ -> UProperty

Property HangulSyllableType_ (Maybe HangulSyllableType)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: HangulSyllableType_ -> Int32 -> Maybe HangulSyllableType

toUProperty :: HangulSyllableType_ -> UProperty

Property JoiningGroup_ (Maybe JoiningGroup)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: JoiningGroup_ -> Int32 -> Maybe JoiningGroup

toUProperty :: JoiningGroup_ -> UProperty

Property JoiningType_ (Maybe JoiningType)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: JoiningType_ -> Int32 -> Maybe JoiningType

toUProperty :: JoiningType_ -> UProperty

Property LineBreak_ (Maybe LineBreak)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: LineBreak_ -> Int32 -> Maybe LineBreak

toUProperty :: LineBreak_ -> UProperty

Property NFCQuickCheck_ (Maybe Bool)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: NFCQuickCheck_ -> Int32 -> Maybe Bool

toUProperty :: NFCQuickCheck_ -> UProperty

Property NFDQuickCheck_ (Maybe Bool)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: NFDQuickCheck_ -> Int32 -> Maybe Bool

toUProperty :: NFDQuickCheck_ -> UProperty

Property NFKCQuickCheck_ (Maybe Bool)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: NFKCQuickCheck_ -> Int32 -> Maybe Bool

toUProperty :: NFKCQuickCheck_ -> UProperty

Property NFKDQuickCheck_ (Maybe Bool)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: NFKDQuickCheck_ -> Int32 -> Maybe Bool

toUProperty :: NFKDQuickCheck_ -> UProperty

Property NumericType_ (Maybe NumericType)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: NumericType_ -> Int32 -> Maybe NumericType

toUProperty :: NumericType_ -> UProperty

Property SentenceBreak_ (Maybe SentenceBreak)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: SentenceBreak_ -> Int32 -> Maybe SentenceBreak

toUProperty :: SentenceBreak_ -> UProperty

Property WordBreak_ (Maybe WordBreak)

Instance details

Defined in Data.Text.ICU.Char

Methods

fromNative :: WordBreak_ -> Int32 -> Maybe WordBreak

toUProperty :: WordBreak_ -> UProperty

Conversion MOT (Exp O) Term Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

Conversion MOT (Exp O) Type Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion TOM (Arg Pattern) (Pat O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b Source #

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 (Maybe BindName) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

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

Methods

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

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

ToConcrete (Maybe Pattern) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

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

Methods

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

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

ToConcrete (Maybe QName) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

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

Methods

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

bindToConcrete :: Maybe QName -> (ConOfAbs (Maybe QName) -> 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 #

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 #

Data a => Data (Maybe a)

Instance details

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Maybe a -> c (Maybe a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Maybe a)

toConstr :: Maybe a -> Constr

dataTypeOf :: Maybe a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Maybe a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Maybe a))

gmapT :: (forall b. Data b => b -> b) -> Maybe a -> Maybe a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Maybe a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Maybe a -> r

gmapQ :: (forall d. Data d => d -> u) -> Maybe a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Maybe a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Maybe a -> m (Maybe a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Maybe a -> m (Maybe a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Maybe a -> m (Maybe a)

Semigroup a => Monoid (Maybe a)

Instance details

Defined in GHC.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.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.Generics

Associated Types

type Rep (Maybe a)
Instance details Defined in GHC.Generics type Rep (Maybe a) = D1 ('MetaData "Maybe" "GHC.Maybe" "base" '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.Generics

Associated Types

type DemoteRep (Maybe a)
Instance details Defined in GHC.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.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.Show

Methods

showsPrec :: Int -> Maybe a -> ShowS

show :: Maybe a -> String

showList :: [Maybe a] -> ShowS

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

Hashable a => Hashable (Maybe a)

Instance details

Defined in Data.Hash.Instances

Methods

hash :: Maybe a -> Hash

NFData a => NFData (Maybe a)

Instance details

Defined in Control.DeepSeq

Methods

rnf :: Maybe a -> ()

Eq a => Eq (Maybe a)

Instance details

Defined in GHC.Maybe

Methods

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

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

Ord a => Ord (Maybe a)

Instance details

Defined in GHC.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 Source #

Hashable64 a => Hashable64 (Maybe a)

Instance details

Defined in Data.Digest.Murmur64

Methods

hash64Add :: Maybe a -> Hash64 -> Hash64 Source #

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

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.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.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.Generics

type Rep1 Maybe = D1 ('MetaData "Maybe" "GHC.Maybe" "base" '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 BindName) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe BindName) = Maybe Name

type ConOfAbs (Maybe Pattern) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe Pattern) = Maybe Pattern

type ConOfAbs (Maybe QName) Source #

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs (Maybe QName) = Maybe Name

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.Generics

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

type Rep (Maybe a)

Instance details

Defined in GHC.Generics

type Rep (Maybe a) = D1 ('MetaData "Maybe" "GHC.Maybe" "base" '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.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] #

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

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

listToMaybe :: [a] -> Maybe a #

maybeToList :: Maybe a -> [a] #

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

isNothing :: Maybe a -> Bool #

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

isJust :: Maybe a -> Bool #