Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.Tokens

# Documentation

data Token Source #

Constructors

TokKeyword Keyword Interval |
TokId (Interval, String) |
TokQId [(Interval, String)] |
TokLiteral Literal |
TokSymbol Symbol Interval |
TokString (Interval, String) |
TokSetN (Interval, Integer) |
TokPropN (Interval, Integer) |
TokTeX (Interval, String) |
TokMarkup (Interval, String) |
TokComment (Interval, String) |
TokDummy |
TokEOF Interval |

Instances

Eq Token Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Token -> Token -> Bool Source # (/=) :: Token -> Token -> Bool Source #
Show Token Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> Token -> ShowS Source # show :: Token -> String Source # showList :: [Token] -> ShowS Source #
HasRange Token Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods getRange :: Token -> Range Source #

data Keyword Source #

Constructors

KwLet |
KwIn |
KwWhere |
KwData |
KwCoData |
KwDo |
KwPostulate |
KwMutual |
KwAbstract |
KwPrivate |
KwInstance |
KwOverlap |
KwOpen |
KwImport |
KwModule |
KwPrimitive |
KwMacro |
KwInfix |
KwInfixL |
KwInfixR |
KwWith |
KwRewrite |
KwSet |
KwProp |
KwForall |
KwRecord |
KwConstructor |
KwField |
KwInductive |
KwCoInductive |
KwEta |
KwNoEta |
KwHiding |
KwUsing |
KwRenaming |
KwTo |
KwPublic |
KwOPTIONS |
KwBUILTIN |
KwLINE |
KwFOREIGN |
KwCOMPILE |
KwIMPOSSIBLE |
KwSTATIC |
KwINJECTIVE |
KwINLINE |
KwNOINLINE |
KwETA |
KwNO_TERMINATION_CHECK |
KwTERMINATING |
KwNON_TERMINATING |
KwWARNING_ON_USAGE |
KwMEASURE |
KwDISPLAY |
KwREWRITE |
KwQuoteGoal |
KwQuoteContext |
KwQuote |
KwQuoteTerm |
KwUnquote |
KwUnquoteDecl |
KwUnquoteDef |
KwSyntax |
KwPatternSyn |
KwTactic |
KwCATCHALL |
KwVariable |
KwNO_POSITIVITY_CHECK |
KwPOLARITY |
KwNO_UNIVERSE_CHECK |

Instances

Eq Keyword Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Keyword -> Keyword -> Bool Source # (/=) :: Keyword -> Keyword -> Bool Source #
Show Keyword Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> Keyword -> ShowS Source # show :: Keyword -> String Source # showList :: [Keyword] -> ShowS Source #

layoutKeywords :: [Keyword] Source #

data Symbol Source #

Constructors

SymDot |
SymSemi |
SymVirtualSemi |
SymBar |
SymColon |
SymArrow |
SymEqual |
SymLambda |
SymUnderscore |
SymQuestionMark |
SymAs |
SymOpenParen |
SymCloseParen |
SymOpenIdiomBracket |
SymCloseIdiomBracket |
SymDoubleOpenBrace |
SymDoubleCloseBrace |
SymOpenBrace |
SymCloseBrace |
SymOpenVirtualBrace |
SymCloseVirtualBrace |
SymOpenPragma |
SymClosePragma |
SymEllipsis |
SymDotDot |
SymEndComment | A misplaced end-comment "-}".

Instances

Eq Symbol Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods (==) :: Symbol -> Symbol -> Bool Source # (/=) :: Symbol -> Symbol -> Bool Source #
Show Symbol Source # |
Instance details Defined in Agda.Syntax.Parser.Tokens Methods showsPrec :: Int -> Symbol -> ShowS Source # show :: Symbol -> String Source # showList :: [Symbol] -> ShowS Source #