Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- data MetaInfo = MetaInfo {
- metaRange :: Range
- metaScope :: ScopeInfo
- metaNumber :: Maybe MetaId
- metaNameSuggestion :: String
- emptyMetaInfo :: MetaInfo
- newtype ExprInfo = ExprRange Range
- exprNoRange :: ExprInfo
- data AppInfo = AppInfo {}
- defaultAppInfo :: Range -> AppInfo
- defaultAppInfo_ :: AppInfo
- data ModuleInfo = ModuleInfo {
- minfoRange :: Range
- minfoAsTo :: Range
- minfoAsName :: Maybe Name
- minfoOpenShort :: Maybe OpenShortHand
- minfoDirective :: Maybe ImportDirective
- newtype LetInfo = LetRange Range
- data DefInfo = DefInfo {}
- mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
- mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo
- data DeclInfo = DeclInfo {}
- data MutualInfo = MutualInfo {}
- newtype LHSInfo = LHSRange Range
- newtype PatInfo = PatRange Range
- patNoRange :: PatInfo
- data ConPatInfo = ConPatInfo {}
- data ConPatLazy
Documentation
Constructors
MetaInfo | |
Fields
|
Instances
Eq MetaInfo Source # | |
Data MetaInfo Source # | |
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 # | |
KillRange MetaInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange MetaInfo Source # | |
Instances
Eq ExprInfo Source # | |
Data ExprInfo Source # | |
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 # | |
Null ExprInfo Source # | |
KillRange ExprInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange ExprInfo Source # | |
Information about application
Constructors
AppInfo | |
Instances
Eq AppInfo Source # | |
Data AppInfo Source # | |
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 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 # | |
Show AppInfo Source # | |
KillRange AppInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange AppInfo Source # | |
LensOrigin AppInfo Source # | |
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 # | |
Defined in Agda.Syntax.Info | |
Data ModuleInfo Source # | |
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 # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS show :: ModuleInfo -> String showList :: [ModuleInfo] -> ShowS | |
KillRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source # | |
HasRange ModuleInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source # | |
UniverseBi Declaration ModuleInfo Source # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleInfo] Source # |
Instances
Eq LetInfo Source # | |
Data LetInfo Source # | |
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 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 # | |
Null LetInfo Source # | |
KillRange LetInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange LetInfo Source # | |
Constructors
DefInfo | |
Fields
|
Instances
Eq DefInfo Source # | |
Data DefInfo Source # | |
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 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 # | |
KillRange DefInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange DefInfo Source # | |
HasRange DefInfo Source # | |
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo Source #
Same as mkDefInfo
but where we can also give the IsInstance
Instances
Eq DeclInfo Source # | |
Data DeclInfo Source # | |
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 # | |
KillRange DeclInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange DeclInfo Source # | |
HasRange DeclInfo Source # | |
data MutualInfo Source #
Constructors
MutualInfo | |
Instances
Eq MutualInfo Source # | |
Defined in Agda.Syntax.Info | |
Data MutualInfo Source # | |
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 # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS show :: MutualInfo -> String showList :: [MutualInfo] -> ShowS | |
Null MutualInfo Source # | Default value for |
Defined in Agda.Syntax.Info | |
KillRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange MutualInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source # |
Instances
Eq LHSInfo Source # | |
Data LHSInfo Source # | |
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 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 # | |
Null LHSInfo Source # | |
KillRange LHSInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
HasRange LHSInfo Source # | |
For a general pattern we remember the source code position.
Instances
Eq PatInfo Source # | |
Data PatInfo Source # | |
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 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 # | |
Null PatInfo Source # | |
KillRange PatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange PatInfo Source # | |
HasRange PatInfo Source # | |
patNoRange :: PatInfo Source #
Empty range for patterns.
data ConPatInfo Source #
Constructor pattern info.
Constructors
ConPatInfo | |
Instances
Eq ConPatInfo Source # | |
Defined in Agda.Syntax.Info | |
Data ConPatInfo Source # | |
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 # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS show :: ConPatInfo -> String showList :: [ConPatInfo] -> ShowS | |
KillRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods | |
SetRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source # | |
HasRange ConPatInfo Source # | |
Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source # | |
EmbPrj ConPatInfo Source # | |
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 # | |
Defined in Agda.Syntax.Info | |
Enum ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods succ :: ConPatLazy -> ConPatLazy pred :: ConPatLazy -> ConPatLazy toEnum :: Int -> ConPatLazy fromEnum :: ConPatLazy -> Int enumFrom :: ConPatLazy -> [ConPatLazy] enumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy] enumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy] enumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy] | |
Eq ConPatLazy Source # | |
Defined in Agda.Syntax.Info | |
Data ConPatLazy Source # | |
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 # | |
Defined in Agda.Syntax.Info Methods compare :: ConPatLazy -> ConPatLazy -> Ordering (<) :: ConPatLazy -> ConPatLazy -> Bool (<=) :: ConPatLazy -> ConPatLazy -> Bool (>) :: ConPatLazy -> ConPatLazy -> Bool (>=) :: ConPatLazy -> ConPatLazy -> Bool max :: ConPatLazy -> ConPatLazy -> ConPatLazy min :: ConPatLazy -> ConPatLazy -> ConPatLazy | |
Show ConPatLazy Source # | |
Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatLazy -> ShowS show :: ConPatLazy -> String showList :: [ConPatLazy] -> ShowS | |
EmbPrj ConPatLazy Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatLazy -> S Int32 Source # icod_ :: ConPatLazy -> S Int32 Source # value :: Int32 -> R ConPatLazy Source # |