Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Parser.Tokens

Synopsis

Documentation

data Token Source #

Constructors

TokKeyword Keyword Interval 
TokId (Interval, String) 
TokQId [(Interval, String)] 
TokLiteral RLiteral 
TokSymbol Symbol Interval 
TokString (Interval, String)

Arbitrary string (not enclosed in double quotes), used in pragmas.

TokTeX (Interval, String) 
TokMarkup (Interval, String) 
TokComment (Interval, String) 
TokDummy 
TokEOF Interval 

Instances

Instances details
HasRange Token Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

getRange :: Token -> Range Source #

Show Token Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

showsPrec :: Int -> Token -> ShowS #

show :: Token -> String #

showList :: [Token] -> ShowS #

Eq Token Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

(==) :: Token -> Token -> Bool #

(/=) :: Token -> Token -> Bool #

data Keyword Source #

Constructors

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

Instances

Instances details
Show Keyword Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

showsPrec :: Int -> Keyword -> ShowS #

show :: Keyword -> String #

showList :: [Keyword] -> ShowS #

Eq Keyword Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

(==) :: Keyword -> Keyword -> Bool #

(/=) :: Keyword -> Keyword -> Bool #

layoutKeywords :: [Keyword] Source #

Unconditional layout keywords.

Some keywords introduce layout only in certain circumstances, these are not included here.

data Symbol Source #

Constructors

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

A misplaced end-comment "-}".

Instances

Instances details
Show Symbol Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

showsPrec :: Int -> Symbol -> ShowS #

show :: Symbol -> String #

showList :: [Symbol] -> ShowS #

Eq Symbol Source # 
Instance details

Defined in Agda.Syntax.Parser.Tokens

Methods

(==) :: Symbol -> Symbol -> Bool #

(/=) :: Symbol -> Symbol -> Bool #