Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Info

Description

An info object contains additional information about a piece of abstract syntax that isn't part of the actual syntax. For instance, it might contain the source code position of an expression or the concrete syntax that an internal expression originates from.

Synopsis

Documentation

data MetaInfo Source #

Instances

Instances details
Eq MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaInfo -> c MetaInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaInfo Source #

toConstr :: MetaInfo -> Constr Source #

dataTypeOf :: MetaInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> MetaInfo -> MetaInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MetaInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source #

Show MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

newtype ExprInfo Source #

Constructors

ExprRange Range 

Instances

Instances details
Eq ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExprInfo -> c ExprInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExprInfo Source #

toConstr :: ExprInfo -> Constr Source #

dataTypeOf :: ExprInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExprInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> ExprInfo -> ExprInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ExprInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExprInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source #

Show ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data AppInfo Source #

Information about application

Constructors

AppInfo 

Fields

Instances

Instances details
Eq AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AppInfo -> c AppInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AppInfo Source #

toConstr :: AppInfo -> Constr Source #

dataTypeOf :: AppInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AppInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> AppInfo -> AppInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AppInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AppInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source #

Ord AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Show AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

LensOrigin AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

defaultAppInfo :: Range -> AppInfo Source #

Default is system inserted and prefer parens.

defaultAppInfo_ :: AppInfo Source #

AppInfo with no range information.

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

Instances

Instances details
Eq ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleInfo -> c ModuleInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleInfo Source #

toConstr :: ModuleInfo -> Constr Source #

dataTypeOf :: ModuleInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> ModuleInfo -> ModuleInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ModuleInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo Source #

Show ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

UniverseBi Declaration ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

newtype LetInfo Source #

Constructors

LetRange Range 

Instances

Instances details
Eq LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetInfo -> c LetInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetInfo Source #

toConstr :: LetInfo -> Constr Source #

dataTypeOf :: LetInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> LetInfo -> LetInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LetInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LetInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source #

Show LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data DefInfo' t Source #

Instances

Instances details
Eq t => Eq (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: DefInfo' t -> DefInfo' t -> Bool Source #

(/=) :: DefInfo' t -> DefInfo' t -> Bool Source #

Data t => Data (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefInfo' t -> c (DefInfo' t) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefInfo' t) Source #

toConstr :: DefInfo' t -> Constr Source #

dataTypeOf :: DefInfo' t -> DataType Source #

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (DefInfo' t)) Source #

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (DefInfo' t)) Source #

gmapT :: (forall b. Data b => b -> b) -> DefInfo' t -> DefInfo' t Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo' t -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo' t -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DefInfo' t -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DefInfo' t -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t) Source #

Show t => Show (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange t => KillRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DefInfo' t -> DefInfo' t Source #

HasRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range Source #

AnyIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

LensIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t Source #

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo Source #

Constructors

DeclInfo 

Fields

Instances

Instances details
Eq DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclInfo -> c DeclInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclInfo Source #

toConstr :: DeclInfo -> Constr Source #

dataTypeOf :: DeclInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> DeclInfo -> DeclInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DeclInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source #

Show DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data MutualInfo Source #

Instances

Instances details
Eq MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualInfo -> c MutualInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualInfo Source #

toConstr :: MutualInfo -> Constr Source #

dataTypeOf :: MutualInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> MutualInfo -> MutualInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MutualInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source #

Show MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null MutualInfo Source #

Default value for MutualInfo.

Instance details

Defined in Agda.Syntax.Info

KillRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data LHSInfo Source #

Constructors

LHSInfo 

Instances

Instances details
Eq LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSInfo -> c LHSInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSInfo Source #

toConstr :: LHSInfo -> Constr Source #

dataTypeOf :: LHSInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHSInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> LHSInfo -> LHSInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LHSInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source #

Show LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

newtype PatInfo Source #

For a general pattern we remember the source code position.

Constructors

PatRange Range 

Instances

Instances details
Eq PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatInfo -> c PatInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatInfo Source #

toConstr :: PatInfo -> Constr Source #

dataTypeOf :: PatInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> PatInfo -> PatInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> PatInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PatInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source #

Show PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

Constructor pattern info.

Constructors

ConPatInfo 

Fields

Instances

Instances details
Eq ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Data ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatInfo -> c ConPatInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatInfo Source #

toConstr :: ConPatInfo -> Constr Source #

dataTypeOf :: ConPatInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatInfo) Source #

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

gmapT :: (forall b. Data b => b -> b) -> ConPatInfo -> ConPatInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatInfo -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConPatInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo Source #

Show ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

EmbPrj ConPatInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

data ConPatLazy Source #

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy

Dotted constructor.

ConPatEager

Ordinary constructor.

Instances

Instances details
Bounded ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Enum ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Eq ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Data ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatLazy -> c ConPatLazy Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatLazy Source #

toConstr :: ConPatLazy -> Constr Source #

dataTypeOf :: ConPatLazy -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatLazy) Source #

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

gmapT :: (forall b. Data b => b -> b) -> ConPatLazy -> ConPatLazy Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatLazy -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatLazy -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConPatLazy -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatLazy -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy Source #

Ord ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Show ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

EmbPrj ConPatLazy Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract