Agda.Syntax.Common.Aspect

Documentation

data Induction

Constructors

Inductive

CoInductive

Instances

PatternMatchingAllowed Induction

Defined in Agda.Syntax.Common

Methods

patternMatchingAllowed :: Induction -> Bool

Pretty Induction

Defined in Agda.Syntax.Common

Methods

pretty :: Induction -> Doc

prettyPrec :: Int -> Induction -> Doc

prettyList :: [Induction] -> Doc

HasRange Induction

Defined in Agda.Syntax.Common

Methods

getRange :: Induction -> Range

KillRange Induction

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Induction

EmbPrj Induction

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32

icod_ :: Induction -> S Int32

value :: Int32 -> R Induction

Show Induction

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Induction -> ShowS

show :: Induction -> String

showList :: [Induction] -> ShowS

NFData Induction

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: Induction -> ()

Eq Induction

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Induction -> Induction -> Bool

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

Ord Induction

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: Induction -> Induction -> Ordering

(<) :: Induction -> Induction -> Bool

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

(>) :: Induction -> Induction -> Bool

(>=) :: Induction -> Induction -> Bool

max :: Induction -> Induction -> Induction

min :: Induction -> Induction -> Induction

data Aspect

Constructors

Comment

Keyword

String

Number

Hole

Symbol

Symbols like forall, =, ->, etc.

PrimitiveType

Things like Set and Prop.

Name (Maybe NameKind) Bool

Is the name an operator part?

Pragma

Text occurring in pragmas that does not have a more specific aspect.

Background

Non-code contents in literate Agda

Markup

Delimiters used to separate the Agda code blocks from the other contents in literate Agda

Instances

EmbPrj Aspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32

icod_ :: Aspect -> S Int32

value :: Int32 -> R Aspect

Semigroup Aspect

NameKind in Name can get more precise.

Defined in Agda.Syntax.Common.Aspect

Methods

(<>) :: Aspect -> Aspect -> Aspect

sconcat :: NonEmpty Aspect -> Aspect

stimes :: Integral b => b -> Aspect -> Aspect

Generic Aspect

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspect :: Type -> Type

Methods

from :: Aspect -> Rep Aspect x

to :: Rep Aspect x -> Aspect

Show Aspect

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspect -> ShowS

show :: Aspect -> String

showList :: [Aspect] -> ShowS

NFData Aspect

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> ()

Eq Aspect

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Aspect -> Aspect -> Bool

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

type Rep Aspect

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-inplace" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

data NameKind

NameKinds are figured out during scope checking.

Constructors

Bound

Bound variable.

Generalizable

Generalizable variable. (This includes generalizable variables that have been generalized).

Constructor Induction

Inductive or coinductive constructor.

Datatype

Field

Record field.

Function

Module

Module name.

Postulate

Primitive

Primitive.

Record

Record type.

Argument

Named argument, like x in {x = v}

Macro

Macro.

Instances

EmbPrj NameKind

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32

icod_ :: NameKind -> S Int32

value :: Int32 -> R NameKind

Semigroup NameKind

Some NameKinds are more informative than others.

Defined in Agda.Syntax.Common.Aspect

Methods

(<>) :: NameKind -> NameKind -> NameKind

sconcat :: NonEmpty NameKind -> NameKind

stimes :: Integral b => b -> NameKind -> NameKind

Generic NameKind

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep NameKind :: Type -> Type

Methods

from :: NameKind -> Rep NameKind x

to :: Rep NameKind x -> NameKind

Show NameKind

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> NameKind -> ShowS

show :: NameKind -> String

showList :: [NameKind] -> ShowS

NFData NameKind

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: NameKind -> ()

Eq NameKind

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: NameKind -> NameKind -> Bool

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

type Rep NameKind

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-inplace" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

data OtherAspect

Other aspects, generated by type checking. (These can overlap with each other and with Aspects.)

Constructors

Error

ErrorWarning

A warning that is considered fatal in the end.

DottedPattern

UnsolvedMeta

UnsolvedConstraint

Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.

TerminationProblem

PositivityProblem

Deadcode

Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc.

ShadowingInTelescope

Used for shadowed repeated variable names in telescopes.

CoverageProblem

IncompletePattern

When this constructor is used it is probably a good idea to include a note explaining why the pattern is incomplete.

TypeChecks

Code which is being type-checked.

MissingDefinition

Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode.

CatchallClause

ConfluenceProblem

Instances

EmbPrj OtherAspect

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32

icod_ :: OtherAspect -> S Int32

value :: Int32 -> R OtherAspect

Bounded OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

minBound :: OtherAspect

maxBound :: OtherAspect

Enum OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

succ :: OtherAspect -> OtherAspect

pred :: OtherAspect -> OtherAspect

toEnum :: Int -> OtherAspect

fromEnum :: OtherAspect -> Int

enumFrom :: OtherAspect -> [OtherAspect]

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect]

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect]

Generic OtherAspect

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep OtherAspect :: Type -> Type

Methods

from :: OtherAspect -> Rep OtherAspect x

to :: Rep OtherAspect x -> OtherAspect

Show OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> OtherAspect -> ShowS

show :: OtherAspect -> String

showList :: [OtherAspect] -> ShowS

NFData OtherAspect

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: OtherAspect -> ()

Eq OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: OtherAspect -> OtherAspect -> Bool

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

Ord OtherAspect

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: OtherAspect -> OtherAspect -> Ordering

(<) :: OtherAspect -> OtherAspect -> Bool

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

(>) :: OtherAspect -> OtherAspect -> Bool

(>=) :: OtherAspect -> OtherAspect -> Bool

max :: OtherAspect -> OtherAspect -> OtherAspect

min :: OtherAspect -> OtherAspect -> OtherAspect

type Rep OtherAspect

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-inplace" 'False) (((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Aspects

Syntactic aspects of the code. (These cannot overlap.)

Meta information which can be associated with a character/character range.

Constructors

Aspects

Fields

• aspect :: Maybe Aspect
• otherAspects :: Set OtherAspect
• note :: String

  This note, if not null, can be displayed as a tool-tip or something like that. It should contain useful information about the range (like the module containing a certain identifier, or the fixity of an operator).

• definitionSite :: Maybe DefinitionSite

  The definition site of the annotated thing, if applicable and known.

• tokenBased :: !TokenBased

  Is this entry token-based?

Instances

EncodeTCM Doc

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value

Underscore Doc

Defined in Agda.Syntax.Common

Methods

underscore :: Doc

isUnderscore :: Doc -> Bool

ReportS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m ()

TraceS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c

EmbPrj Aspects

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32

icod_ :: Aspects -> S Int32

value :: Int32 -> R Aspects

EmbPrj Doc

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32

icod_ :: Doc -> S Int32

value :: Int32 -> R Doc

Monoid Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: Aspects

mappend :: Aspects -> Aspects -> Aspects

mconcat :: [Aspects] -> Aspects

Semigroup Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: Aspects -> Aspects -> Aspects

sconcat :: NonEmpty Aspects -> Aspects

stimes :: Integral b => b -> Aspects -> Aspects

Generic Aspects

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspects :: Type -> Type

Methods

from :: Aspects -> Rep Aspects x

to :: Rep Aspects x -> Aspects

Show Aspects

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspects -> ShowS

show :: Aspects -> String

showList :: [Aspects] -> ShowS

NFData Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspects -> ()

Eq Aspects

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: Aspects -> Aspects -> Bool

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

ToJSON Doc

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value

toEncoding :: Doc -> Encoding

toJSONList :: [Doc] -> Value

toEncodingList :: [Doc] -> Encoding

omitField :: Doc -> Bool

IsBasicRangeMap Aspects PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap

toMap :: PositionMap -> IntMap Aspects

toList :: PositionMap -> [(Range, Aspects)]

coveringRange :: PositionMap -> Maybe Range

IsBasicRangeMap Aspects RangePair

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair

toMap :: RangePair -> IntMap Aspects

toList :: RangePair -> [(Range, Aspects)]

coveringRange :: RangePair -> Maybe Range

Convert PositionMap (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects

IsBasicRangeMap Aspects (DelayedMerge PositionMap)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap

toMap :: DelayedMerge PositionMap -> IntMap Aspects

toList :: DelayedMerge PositionMap -> [(Range, Aspects)]

coveringRange :: DelayedMerge PositionMap -> Maybe Range

IsBasicRangeMap Aspects (DelayedMerge RangePair)

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair

toMap :: DelayedMerge RangePair -> IntMap Aspects

toList :: DelayedMerge RangePair -> [(Range, Aspects)]

coveringRange :: DelayedMerge RangePair -> Maybe Range

ReportS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()

ReportS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m ()

ReportS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m ()

TraceS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c

TraceS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c

TraceS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c

Null (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

empty :: AbsToCon Doc

null :: AbsToCon Doc -> Bool

Null (TCM Doc)

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc

null :: TCM Doc -> Bool

IsString (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fromString :: String -> AbsToCon Doc

Semigroup (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc

sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc

stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc

Semigroup (TCM Doc)

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

Defined in Agda.TypeChecking.Pretty

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

Convert (DelayedMerge PositionMap) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects

Convert (DelayedMerge RangePair) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects

Convert (RangeMap Aspects) (RangeMap Aspects)

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: RangeMap Aspects -> RangeMap Aspects

Monad m => Null (PureConversionT m Doc)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc

null :: PureConversionT m Doc -> Bool

type Rep Aspects

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

data DefinitionSite

Constructors

DefinitionSite

Fields

• defSiteModule :: TopLevelModuleName

  The defining module.

• defSitePos :: Int

  The file position in that module. File positions are counted from 1.

• defSiteHere :: Bool

  Has this DefinitionSite been created at the defining site of the name?

• defSiteAnchor :: Maybe String

  A pretty name for the HTML linking.

Instances

EmbPrj DefinitionSite

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32

icod_ :: DefinitionSite -> S Int32

value :: Int32 -> R DefinitionSite

Semigroup DefinitionSite

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite

sconcat :: NonEmpty DefinitionSite -> DefinitionSite

stimes :: Integral b => b -> DefinitionSite -> DefinitionSite

Generic DefinitionSite

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep DefinitionSite :: Type -> Type

Methods

from :: DefinitionSite -> Rep DefinitionSite x

to :: Rep DefinitionSite x -> DefinitionSite

Show DefinitionSite

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> DefinitionSite -> ShowS

show :: DefinitionSite -> String

showList :: [DefinitionSite] -> ShowS

NFData DefinitionSite

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: DefinitionSite -> ()

Eq DefinitionSite

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: DefinitionSite -> DefinitionSite -> Bool

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

type Rep DefinitionSite

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

data TokenBased

Is the highlighting "token-based", i.e. based only on information from the lexer?

Constructors

TokenBased

NotOnlyTokenBased

Instances

EncodeTCM TokenBased

Defined in Agda.Interaction.Highlighting.JSON

Methods

encodeTCM :: TokenBased -> TCM Value

EmbPrj TokenBased

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32

icod_ :: TokenBased -> S Int32

value :: Int32 -> R TokenBased

Monoid TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: TokenBased

mappend :: TokenBased -> TokenBased -> TokenBased

mconcat :: [TokenBased] -> TokenBased

Semigroup TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: TokenBased -> TokenBased -> TokenBased

sconcat :: NonEmpty TokenBased -> TokenBased

stimes :: Integral b => b -> TokenBased -> TokenBased

Show TokenBased

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> TokenBased -> ShowS

show :: TokenBased -> String

showList :: [TokenBased] -> ShowS

Eq TokenBased

Defined in Agda.Syntax.Common.Aspect

Methods

(==) :: TokenBased -> TokenBased -> Bool

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

ToJSON TokenBased

Defined in Agda.Interaction.Highlighting.JSON

Methods

toJSON :: TokenBased -> Value

toEncoding :: TokenBased -> Encoding

toJSONList :: [TokenBased] -> Value

toEncodingList :: [TokenBased] -> Encoding

omitField :: TokenBased -> Bool