Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Common.Aspect

Synopsis

data Induction
- = Inductive
- | CoInductive
data Aspect
- = Comment
- | Keyword
- | String
- | Number
- | Hole
- | Symbol
- | PrimitiveType
- | Name (Maybe NameKind) Bool
- | Pragma
- | Background
- | Markup
data NameKind
- = Bound
- | Generalizable
- | Constructor Induction
- | Datatype
- | Field
- | Function
- | Module
- | Postulate
- | Primitive
- | Record
- | Argument
- | Macro
data OtherAspect
- = Error
- | ErrorWarning
- | DottedPattern
- | UnsolvedMeta
- | UnsolvedConstraint
- | TerminationProblem
- | PositivityProblem
- | Deadcode
- | ShadowingInTelescope
- | CoverageProblem
- | IncompletePattern
- | TypeChecks
- | MissingDefinition
- | InstanceProblem
- | CosmeticProblem
- | CatchallClause
- | ConfluenceProblem
data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: String
- definitionSite :: Maybe DefinitionSite
- tokenBased :: !TokenBased
}
data DefinitionSite = DefinitionSite {
- defSiteModule :: TopLevelModuleName' Range
- defSitePos :: Int
- defSiteHere :: Bool
- defSiteAnchor :: Maybe String
}
data TokenBased
- = TokenBased
- | NotOnlyTokenBased

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 Word32 Source # icod_ :: Induction -> S Word32 Source # value :: Word32 -> R Induction Source #
NFData Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: Induction -> () #
Show Induction Source #
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Induction -> ShowS # show :: Induction -> String # showList :: [Induction] -> ShowS #
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 Word32 Source #

icod_ :: Aspect -> S Word32 Source #

value :: Word32 -> R Aspect Source #

NFData Aspect Source #

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

rnf :: Aspect -> () #

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

Instance details

Defined in Agda.Syntax.Common.Aspect

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 #

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

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.