Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Common.Aspect

Synopsis

Documentation

data Induction Source #

Constructors

Inductive 
CoInductive 

Instances

Instances details
PatternMatchingAllowed Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

patternMatchingAllowed :: Induction -> Bool Source #

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Induction -> Doc Source #

prettyPrec :: Int -> Induction -> Doc Source #

prettyList :: [Induction] -> Doc Source #

HasRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

getRange :: Induction -> Range Source #

KillRange Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

killRange :: KillRangeT Induction Source #

EmbPrj Induction Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Induction -> S Int32 Source #

icod_ :: Induction -> S Int32 Source #

value :: Int32 -> R Induction Source #

Show Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Induction -> ShowS #

show :: Induction -> String #

showList :: [Induction] -> ShowS #

NFData Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: Induction -> () #

Eq Induction Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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

Ord Induction Source # 
Instance details

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 Source #

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

Instances details
EmbPrj Aspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspect -> S Int32 Source #

icod_ :: Aspect -> S Int32 Source #

value :: Int32 -> R Aspect Source #

Semigroup Aspect Source #

NameKind in Name can get more precise.

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

sconcat :: NonEmpty Aspect -> Aspect #

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

Generic Aspect Source # 
Instance details

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

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspect -> ShowS #

show :: Aspect -> String #

showList :: [Aspect] -> ShowS #

NFData Aspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> () #

Eq Aspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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

type Rep Aspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" '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 Source #

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

Instances details
EmbPrj NameKind Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: NameKind -> S Int32 Source #

icod_ :: NameKind -> S Int32 Source #

value :: Int32 -> R NameKind Source #

Semigroup NameKind Source #

Some NameKinds are more informative than others.

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

sconcat :: NonEmpty NameKind -> NameKind #

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

Generic NameKind Source # 
Instance details

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

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> NameKind -> ShowS #

show :: NameKind -> String #

showList :: [NameKind] -> ShowS #

NFData NameKind Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

rnf :: NameKind -> () #

Eq NameKind Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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

type Rep NameKind Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" '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 Source #

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

Instances details
EmbPrj OtherAspect Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: OtherAspect -> S Int32 Source #

icod_ :: OtherAspect -> S Int32 Source #

value :: Int32 -> R OtherAspect Source #

Bounded OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

minBound :: OtherAspect #

maxBound :: OtherAspect #

Enum OtherAspect Source # 
Instance details

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

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

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> OtherAspect -> ShowS #

show :: OtherAspect -> String #

showList :: [OtherAspect] -> ShowS #

NFData OtherAspect Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: OtherAspect -> () #

Eq OtherAspect Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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

Ord OtherAspect Source # 
Instance details

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

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" '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 Source #

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

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

Constructors

Aspects 

Fields

Instances

Instances details
EncodeTCM Doc Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value Source #

Underscore Doc Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: Doc Source #

isUnderscore :: Doc -> Bool Source #

ReportS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

EmbPrj Aspects Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Aspects -> S Int32 Source #

icod_ :: Aspects -> S Int32 Source #

value :: Int32 -> R Aspects Source #

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32 Source #

icod_ :: Doc -> S Int32 Source #

value :: Int32 -> R Doc Source #

ToJSON Doc Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value #

toEncoding :: Doc -> Encoding #

toJSONList :: [Doc] -> Value #

toEncodingList :: [Doc] -> Encoding #

omitField :: Doc -> Bool #

Monoid Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: Aspects #

mappend :: Aspects -> Aspects -> Aspects #

mconcat :: [Aspects] -> Aspects #

Semigroup Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty Aspects -> Aspects #

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

Generic Aspects Source # 
Instance details

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

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> Aspects -> ShowS #

show :: Aspects -> String #

showList :: [Aspects] -> ShowS #

NFData Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspects -> () #

Eq Aspects Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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

IsBasicRangeMap Aspects PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> PositionMap Source #

toMap :: PositionMap -> IntMap Aspects Source #

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

coveringRange :: PositionMap -> Maybe Range Source #

IsBasicRangeMap Aspects RangePair Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> RangePair Source #

toMap :: RangePair -> IntMap Aspects Source #

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

coveringRange :: RangePair -> Maybe Range Source #

Convert PositionMap (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: PositionMap -> RangeMap Aspects Source #

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source #

toMap :: DelayedMerge PositionMap -> IntMap Aspects Source #

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

coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #

IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source #

toMap :: DelayedMerge RangePair -> IntMap Aspects Source #

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

coveringRange :: DelayedMerge RangePair -> Maybe Range Source #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

Null (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

empty :: AbsToCon Doc Source #

null :: AbsToCon Doc -> Bool Source #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc Source #

null :: TCM Doc -> Bool Source #

IsString (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fromString :: String -> AbsToCon Doc #

Semigroup (AbsToCon Doc) Source # 
Instance details

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) Source #

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

Instance details

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

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #

Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

Convert (RangeMap Aspects) (RangeMap Aspects) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

convert :: RangeMap Aspects -> RangeMap Aspects Source #

Monad m => Null (PureConversionT m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc Source #

null :: PureConversionT m Doc -> Bool Source #

type Rep Aspects Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" '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 Source #

Constructors

DefinitionSite 

Fields

Instances

Instances details
EmbPrj DefinitionSite Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: DefinitionSite -> S Int32 Source #

icod_ :: DefinitionSite -> S Int32 Source #

value :: Int32 -> R DefinitionSite Source #

Semigroup DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty DefinitionSite -> DefinitionSite #

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

Generic DefinitionSite Source # 
Instance details

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

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> DefinitionSite -> ShowS #

show :: DefinitionSite -> String #

showList :: [DefinitionSite] -> ShowS #

NFData DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: DefinitionSite -> () #

Eq DefinitionSite Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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

type Rep DefinitionSite Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.6.4.3-Ljl5wY0h7qEDjMk20qhhzf" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: 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 Source #

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

Constructors

TokenBased 
NotOnlyTokenBased 

Instances

Instances details
EncodeTCM TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.JSON

Methods

encodeTCM :: TokenBased -> TCM Value Source #

EmbPrj TokenBased Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: TokenBased -> S Int32 Source #

icod_ :: TokenBased -> S Int32 Source #

value :: Int32 -> R TokenBased Source #

ToJSON TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.JSON

Methods

toJSON :: TokenBased -> Value #

toEncoding :: TokenBased -> Encoding #

toJSONList :: [TokenBased] -> Value #

toEncodingList :: [TokenBased] -> Encoding #

omitField :: TokenBased -> Bool #

Monoid TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

mempty :: TokenBased #

mappend :: TokenBased -> TokenBased -> TokenBased #

mconcat :: [TokenBased] -> TokenBased #

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty TokenBased -> TokenBased #

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

Show TokenBased Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

showsPrec :: Int -> TokenBased -> ShowS #

show :: TokenBased -> String #

showList :: [TokenBased] -> ShowS #

Eq TokenBased Source # 
Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

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