| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common.Aspect
Synopsis
- data Induction
- data Aspect
- data NameKind
- data OtherAspect
- data Aspects = Aspects {}
- data DefinitionSite = DefinitionSite {}
- data TokenBased
Documentation
Constructors
| Inductive | |
| CoInductive |
Instances
| PatternMatchingAllowed Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| Pretty Induction Source # | |
| HasRange Induction Source # | |
| KillRange Induction Source # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj Induction Source # | |
| Show Induction Source # | |
| NFData Induction Source # | |
Defined in Agda.Syntax.Common.Aspect | |
| Eq Induction Source # | |
| Ord Induction 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
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
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 |
| 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
Syntactic aspects of the code. (These cannot overlap.)
Meta information which can be associated with a character/character range.
Constructors
| Aspects | |
Fields
| |
Instances
data DefinitionSite Source #
Constructors
| DefinitionSite | |
Fields
| |
Instances
data TokenBased Source #
Is the highlighting "token-based", i.e. based only on information from the lexer?
Constructors
| TokenBased | |
| NotOnlyTokenBased |