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

Safe Haskell | None

Agda.Syntax.Parser.Tokens

# Documentation

data Token

Constructors

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

Instances

Eq Token |
Show Token |
HasRange Token |

data Keyword

Constructors

KwLet |
KwIn |
KwWhere |
KwData |
KwCoData |
KwPostulate |
KwMutual |
KwAbstract |
KwPrivate |
KwOpen |
KwImport |
KwModule |
KwPrimitive |
KwInfix |
KwInfixL |
KwInfixR |
KwWith |
KwRewrite |
KwSet |
KwProp |
KwForall |
KwRecord |
KwConstructor |
KwField |
KwInductive |
KwCoInductive |
KwHiding |
KwUsing |
KwRenaming |
KwTo |
KwPublic |
KwOPTIONS |
KwBUILTIN |
KwLINE |
KwCOMPILED_DATA |
KwCOMPILED_TYPE |
KwCOMPILED |
KwCOMPILED_EPIC |
KwCOMPILED_JS |
KwIMPORT |
KwIMPOSSIBLE |
KwETA |
KwNO_TERMINATION_CHECK |
KwSTATIC |
KwQuoteGoal |
KwQuote |
KwQuoteTerm |
KwUnquote |
KwSyntax |
KwPatternSyn |

Instances

Eq Keyword |
Show Keyword |

layoutKeywords :: [Keyword]

data Symbol

Constructors

SymDot |
SymSemi |
SymVirtualSemi |
SymBar |
SymColon |
SymArrow |
SymEqual |
SymLambda |
SymUnderscore |
SymQuestionMark |
SymAs |
SymOpenParen |
SymCloseParen |
SymDoubleOpenBrace |
SymDoubleCloseBrace |
SymOpenBrace |
SymCloseBrace |
SymOpenVirtualBrace |
SymCloseVirtualBrace |
SymOpenPragma |
SymClosePragma |
SymEllipsis |
SymDotDot |

Instances

Eq Symbol |
Show Symbol |