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

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) 
TokTeX (Interval, String) 
TokComment (Interval, String) 
TokDummy 
TokEOF 

Instances

data Keyword Source

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 
KwHiding 
KwUsing 
KwRenaming 
KwTo 
KwPublic 
KwOPTIONS 
KwBUILTIN 
KwLINE 
KwCOMPILED_DATA 
KwCOMPILED_TYPE 
KwCOMPILED 
KwIMPORT 
KwIMPOSSIBLE 
KwETA 
KwQuoteGoal 
KwQuote 
KwSyntax 

Instances

layoutKeywords :: [Keyword]Source

data Symbol Source

Constructors

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

Instances