Hoogle Search
Within LTS Haskell 24.52 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
ParseOk :: ParseState -> a -> ParseResult aAgda Agda.Syntax.Parser.Monad No documentation available.
-
Agda Agda.Syntax.Parser.Monad The result of parsing something.
-
Agda Agda.Syntax.Parser.Monad The parser state. Contains everything the parser and the lexer could ever need.
-
Agda Agda.Syntax.Parser.Monad Warnings for parsing.
-
Agda Agda.Syntax.Parser.Monad The parse monad.
module Agda.Syntax.Parser.
Parser The parser is generated by Happy (http://www.haskell.org/happy). - - Ideally, ranges should be as precise as possible, to get messages that - emphasize precisely the faulting term(s) upon error. - - However, interactive highlighting is only applied at the end of each - mutual block, keywords are only highlighted once (see - Decl). So if the ranges of two declarations - interleave, one must ensure that keyword ranges are not included in - the intersection. (Otherwise they are uncolored by the interactive - highlighting.) -
-
Position information for syntax. Crucial for giving good error messages.
Pn :: a -> Word32 -> Word32 -> Word32 -> Position' aAgda Agda.Syntax.Position No documentation available.
type
Position = Position' SrcFileAgda Agda.Syntax.Position No documentation available.
-
Agda Agda.Syntax.Position Represents a point in the input. If two positions have the same srcFile and posPos components, then the final two components should be the same as well, but since this can be hard to enforce the program should not rely too much on the last two components; they are mainly there to improve error messages for the user. Note the invariant which positions have to satisfy: positionInvariant.