Agda-2.6.20240714: 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 MetaKind Source #

Kind of a meta: the method how to solve it.

Constructors

InstanceMeta

Meta variable solved by instance search.

UnificationMeta

Meta variable solved by unification (default).

Instances

Instances details
Null MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: MetaKind Source #

null :: MetaKind -> Bool Source #

NFData MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: MetaKind -> ()

Generic MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep MetaKind 
Instance details

Defined in Agda.Syntax.Info

type Rep MetaKind = D1 ('MetaData "MetaKind" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "InstanceMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationMeta" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: MetaKind -> Rep MetaKind x

to :: Rep MetaKind x -> MetaKind

Show MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MetaKind -> ShowS

show :: MetaKind -> String

showList :: [MetaKind] -> ShowS

Eq MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(==) :: MetaKind -> MetaKind -> Bool

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

type Rep MetaKind Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MetaKind = D1 ('MetaData "MetaKind" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "InstanceMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationMeta" 'PrefixI 'False) (U1 :: Type -> Type))

hidingToMetaKind :: Hiding -> MetaKind Source #

Default meta kind from its Hiding context.

type MetaNameSuggestion = String Source #

Name suggestion for meta variable. Empty string means no suggestion.

data MetaInfo Source #

Information associated to a meta variable in the abstract syntax.

Instances

Instances details
HasRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: MetaInfo Source #

null :: MetaInfo -> Bool Source #

NFData MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: MetaInfo -> ()

Generic MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep MetaInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "MetaInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "metaRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "metaScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo)) :*: (S1 ('MetaSel ('Just "metaNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe MetaId)) :*: (S1 ('MetaSel ('Just "metaNameSuggestion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaNameSuggestion) :*: S1 ('MetaSel ('Just "metaKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaKind)))))

Methods

from :: MetaInfo -> Rep MetaInfo x

to :: Rep MetaInfo x -> MetaInfo

Show MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MetaInfo -> ShowS

show :: MetaInfo -> String

showList :: [MetaInfo] -> ShowS

Eq MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

type Rep MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "MetaInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "metaRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "metaScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo)) :*: (S1 ('MetaSel ('Just "metaNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe MetaId)) :*: (S1 ('MetaSel ('Just "metaNameSuggestion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaNameSuggestion) :*: S1 ('MetaSel ('Just "metaKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaKind)))))

newtype ExprInfo Source #

Constructors

ExprRange Range 

Instances

Instances details
HasRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: ExprInfo Source #

null :: ExprInfo -> Bool Source #

NFData ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ExprInfo -> ()

Show ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ExprInfo -> ShowS

show :: ExprInfo -> String

showList :: [ExprInfo] -> ShowS

Eq ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

data AppInfo Source #

Information about application

Constructors

AppInfo 

Fields

Instances

Instances details
LensOrigin AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

NFData AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: AppInfo -> ()

Generic AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep AppInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "AppInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "appRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "appOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin) :*: S1 ('MetaSel ('Just "appParens") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference))))

Methods

from :: AppInfo -> Rep AppInfo x

to :: Rep AppInfo x -> AppInfo

Show AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> AppInfo -> ShowS

show :: AppInfo -> String

showList :: [AppInfo] -> ShowS

Eq AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

type Rep AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "AppInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "appRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "appOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin) :*: S1 ('MetaSel ('Just "appParens") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference))))

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
HasRange 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

NFData ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ModuleInfo -> ()

Generic ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep ModuleInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "minfoRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "minfoAsTo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "minfoAsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: (S1 ('MetaSel ('Just "minfoOpenShort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OpenShortHand)) :*: S1 ('MetaSel ('Just "minfoDirective") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportDirective))))))

Methods

from :: ModuleInfo -> Rep ModuleInfo x

to :: Rep ModuleInfo x -> ModuleInfo

Show ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ModuleInfo -> ShowS

show :: ModuleInfo -> String

showList :: [ModuleInfo] -> ShowS

Eq ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

type Rep ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "minfoRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "minfoAsTo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "minfoAsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: (S1 ('MetaSel ('Just "minfoOpenShort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OpenShortHand)) :*: S1 ('MetaSel ('Just "minfoDirective") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportDirective))))))

newtype LetInfo Source #

Constructors

LetRange Range 

Instances

Instances details
HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: LetInfo Source #

null :: LetInfo -> Bool Source #

NFData LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: LetInfo -> ()

Show LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LetInfo -> ShowS

show :: LetInfo -> String

showList :: [LetInfo] -> ShowS

Eq LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

data DefInfo' t Source #

Instances

Instances details
AllAreOpaque (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

AnyIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

LensIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

LensIsOpaque (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range Source #

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 #

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

Defined in Agda.Syntax.Info

Methods

rnf :: DefInfo' t -> ()

Generic (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep (DefInfo' t) 
Instance details

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DefInfo" 'PrefixI 'True) (((S1 ('MetaSel ('Just "defFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity') :*: S1 ('MetaSel ('Just "defAccess") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Just "defAbstract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Just "defOpaque") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsOpaque))) :*: ((S1 ('MetaSel ('Just "defInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Just "defMacro") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)) :*: (S1 ('MetaSel ('Just "defInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclInfo) :*: S1 ('MetaSel ('Just "defTactic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TacticAttribute' t))))))

Methods

from :: DefInfo' t -> Rep (DefInfo' t) x

to :: Rep (DefInfo' t) x -> DefInfo' t

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

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DefInfo' t -> ShowS

show :: DefInfo' t -> String

showList :: [DefInfo' t] -> ShowS

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

Defined in Agda.Syntax.Info

Methods

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

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

type Rep (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DefInfo" 'PrefixI 'True) (((S1 ('MetaSel ('Just "defFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity') :*: S1 ('MetaSel ('Just "defAccess") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access)) :*: (S1 ('MetaSel ('Just "defAbstract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract) :*: S1 ('MetaSel ('Just "defOpaque") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsOpaque))) :*: ((S1 ('MetaSel ('Just "defInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Just "defMacro") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)) :*: (S1 ('MetaSel ('Just "defInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclInfo) :*: S1 ('MetaSel ('Just "defTactic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TacticAttribute' t))))))

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
HasRange 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

NFData DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: DeclInfo -> ()

Generic DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep DeclInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DeclInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "declName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "declRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

Methods

from :: DeclInfo -> Rep DeclInfo x

to :: Rep DeclInfo x -> DeclInfo

Show DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DeclInfo -> ShowS

show :: DeclInfo -> String

showList :: [DeclInfo] -> ShowS

Eq DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

type Rep DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "DeclInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "declName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "declRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data MutualInfo Source #

Instances

Instances details
HasRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null MutualInfo Source #

Default value for MutualInfo.

Instance details

Defined in Agda.Syntax.Info

NFData MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: MutualInfo -> ()

Generic MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep MutualInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "MutualInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mutualTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TerminationCheck Name)) :*: S1 ('MetaSel ('Just "mutualCoverageCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Just "mutualPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Just "mutualRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

Methods

from :: MutualInfo -> Rep MutualInfo x

to :: Rep MutualInfo x -> MutualInfo

Show MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MutualInfo -> ShowS

show :: MutualInfo -> String

showList :: [MutualInfo] -> ShowS

Eq MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

type Rep MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "MutualInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mutualTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TerminationCheck Name)) :*: S1 ('MetaSel ('Just "mutualCoverageCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Just "mutualPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Just "mutualRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data LHSInfo Source #

Constructors

LHSInfo 

Instances

Instances details
HasRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

KillRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Null LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: LHSInfo Source #

null :: LHSInfo -> Bool Source #

NFData LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: LHSInfo -> ()

Generic LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep LHSInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis)))

Methods

from :: LHSInfo -> Rep LHSInfo x

to :: Rep LHSInfo x -> LHSInfo

Show LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LHSInfo -> ShowS

show :: LHSInfo -> String

showList :: [LHSInfo] -> ShowS

Eq LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

type Rep LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis)))

newtype PatInfo Source #

For a general pattern we remember the source code position.

Constructors

PatRange Range 

Instances

Instances details
HasRange 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

Null PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

empty :: PatInfo Source #

null :: PatInfo -> Bool Source #

NFData PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: PatInfo -> ()

Monoid PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Semigroup PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

(<>) :: PatInfo -> PatInfo -> PatInfo #

sconcat :: NonEmpty PatInfo -> PatInfo

stimes :: Integral b => b -> PatInfo -> PatInfo

Show PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> PatInfo -> ShowS

show :: PatInfo -> String

showList :: [PatInfo] -> ShowS

Eq PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

Constructor pattern info.

Constructors

ConPatInfo 

Fields

Instances

Instances details
HasRange 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

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 #

NFData ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatInfo -> ()

Generic ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatInfo 
Instance details

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConPatInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "conPatOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConOrigin) :*: (S1 ('MetaSel ('Just "conPatInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Just "conPatLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatLazy))))

Methods

from :: ConPatInfo -> Rep ConPatInfo x

to :: Rep ConPatInfo x -> ConPatInfo

Show ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatInfo -> ShowS

show :: ConPatInfo -> String

showList :: [ConPatInfo] -> ShowS

Eq ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

type Rep ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConPatInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "conPatOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConOrigin) :*: (S1 ('MetaSel ('Just "conPatInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Just "conPatLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatLazy))))

data ConPatLazy Source #

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy

Dotted constructor.

ConPatEager

Ordinary constructor.

Instances

Instances details
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 #

NFData ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatLazy -> ()

Bounded ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Enum ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Generic ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatLazy 
Instance details

Defined in Agda.Syntax.Info

type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: ConPatLazy -> Rep ConPatLazy x

to :: Rep ConPatLazy x -> ConPatLazy

Show ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatLazy -> ShowS

show :: ConPatLazy -> String

showList :: [ConPatLazy] -> ShowS

Eq ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

Ord ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))