Agda-2.6.0.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 #

Constructors

MetaInfo 
Instances
Eq MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: MetaInfo -> MetaInfo -> Bool

(/=) :: MetaInfo -> MetaInfo -> Bool

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

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

toConstr :: MetaInfo -> Constr

dataTypeOf :: MetaInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MetaInfo -> ShowS

show :: MetaInfo -> String

showList :: [MetaInfo] -> ShowS

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
Eq ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: ExprInfo -> ExprInfo -> Bool

(/=) :: ExprInfo -> ExprInfo -> Bool

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

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

toConstr :: ExprInfo -> Constr

dataTypeOf :: ExprInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ExprInfo -> ShowS

show :: ExprInfo -> String

showList :: [ExprInfo] -> ShowS

Null ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: ExprInfo Source #

null :: ExprInfo -> Bool Source #

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
Eq AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: AppInfo -> AppInfo -> Bool

(/=) :: AppInfo -> AppInfo -> Bool

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

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

toConstr :: AppInfo -> Constr

dataTypeOf :: AppInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

compare :: AppInfo -> AppInfo -> Ordering

(<) :: AppInfo -> AppInfo -> Bool

(<=) :: AppInfo -> AppInfo -> Bool

(>) :: AppInfo -> AppInfo -> Bool

(>=) :: AppInfo -> AppInfo -> Bool

max :: AppInfo -> AppInfo -> AppInfo

min :: AppInfo -> AppInfo -> AppInfo

Show AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> AppInfo -> ShowS

show :: AppInfo -> String

showList :: [AppInfo] -> ShowS

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
Eq ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: ModuleInfo -> ModuleInfo -> Bool

(/=) :: ModuleInfo -> ModuleInfo -> Bool

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

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

toConstr :: ModuleInfo -> Constr

dataTypeOf :: ModuleInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ModuleInfo -> ShowS

show :: ModuleInfo -> String

showList :: [ModuleInfo] -> ShowS

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
Eq LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: LetInfo -> LetInfo -> Bool

(/=) :: LetInfo -> LetInfo -> Bool

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

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

toConstr :: LetInfo -> Constr

dataTypeOf :: LetInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LetInfo -> ShowS

show :: LetInfo -> String

showList :: [LetInfo] -> ShowS

Null LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: LetInfo Source #

null :: LetInfo -> Bool Source #

KillRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data DefInfo Source #

Instances
Eq DefInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: DefInfo -> DefInfo -> Bool

(/=) :: DefInfo -> DefInfo -> Bool

Data DefInfo 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 -> c DefInfo

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

toConstr :: DefInfo -> Constr

dataTypeOf :: DefInfo -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> DefInfo -> DefInfo

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

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

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

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

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

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

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

Show DefInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DefInfo -> ShowS

show :: DefInfo -> String

showList :: [DefInfo] -> ShowS

KillRange DefInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange DefInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange DefInfo Source # 
Instance details

Defined in Agda.Syntax.Info

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

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo Source #

Constructors

DeclInfo 

Fields

Instances
Eq DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: DeclInfo -> DeclInfo -> Bool

(/=) :: DeclInfo -> DeclInfo -> Bool

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

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

toConstr :: DeclInfo -> Constr

dataTypeOf :: DeclInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DeclInfo -> ShowS

show :: DeclInfo -> String

showList :: [DeclInfo] -> ShowS

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
Eq MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: MutualInfo -> MutualInfo -> Bool

(/=) :: MutualInfo -> MutualInfo -> Bool

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

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

toConstr :: MutualInfo -> Constr

dataTypeOf :: MutualInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MutualInfo -> ShowS

show :: MutualInfo -> String

showList :: [MutualInfo] -> ShowS

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

newtype LHSInfo Source #

Constructors

LHSRange Range 
Instances
Eq LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: LHSInfo -> LHSInfo -> Bool

(/=) :: LHSInfo -> LHSInfo -> Bool

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

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

toConstr :: LHSInfo -> Constr

dataTypeOf :: LHSInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LHSInfo -> ShowS

show :: LHSInfo -> String

showList :: [LHSInfo] -> ShowS

Null LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: LHSInfo Source #

null :: LHSInfo -> Bool Source #

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
Eq PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: PatInfo -> PatInfo -> Bool

(/=) :: PatInfo -> PatInfo -> Bool

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

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

toConstr :: PatInfo -> Constr

dataTypeOf :: PatInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> PatInfo -> ShowS

show :: PatInfo -> String

showList :: [PatInfo] -> ShowS

Null PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: PatInfo Source #

null :: PatInfo -> Bool Source #

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
Eq ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: ConPatInfo -> ConPatInfo -> Bool

(/=) :: ConPatInfo -> ConPatInfo -> Bool

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

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

toConstr :: ConPatInfo -> Constr

dataTypeOf :: ConPatInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatInfo -> ShowS

show :: ConPatInfo -> String

showList :: [ConPatInfo] -> ShowS

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

Methods

icode :: ConPatInfo -> S Int32 Source #

icod_ :: ConPatInfo -> S Int32 Source #

value :: Int32 -> R ConPatInfo Source #

data ConPatLazy Source #

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy

Dotted constructor.

ConPatEager

Ordinary constructor.

Instances
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

Methods

(==) :: ConPatLazy -> ConPatLazy -> Bool

(/=) :: ConPatLazy -> ConPatLazy -> Bool

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

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

toConstr :: ConPatLazy -> Constr

dataTypeOf :: ConPatLazy -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Show ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatLazy -> ShowS

show :: ConPatLazy -> String

showList :: [ConPatLazy] -> ShowS

EmbPrj ConPatLazy Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32 Source #

icod_ :: ConPatLazy -> S Int32 Source #

value :: Int32 -> R ConPatLazy Source #