Agda.Syntax.Parser.Tokens

Documentation

data Token

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

HasRange Token

Defined in Agda.Syntax.Parser.Tokens

Methods

getRange :: Token -> Range

Show Token

Defined in Agda.Syntax.Parser.Tokens

Methods

showsPrec :: Int -> Token -> ShowS

show :: Token -> String

showList :: [Token] -> ShowS

Eq Token

Defined in Agda.Syntax.Parser.Tokens

Methods

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

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

data Keyword

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

KwOPTIONS

KwBUILTIN

KwLINE

KwFOREIGN

KwCOMPILE

KwIMPOSSIBLE

KwSTATIC

KwINJECTIVE

KwINLINE

KwNOINLINE

KwETA

KwNO_TERMINATION_CHECK

KwTERMINATING

KwNON_TERMINATING

KwNOT_PROJECTION_LIKE

KwNON_COVERING

KwWARNING_ON_USAGE

KwWARNING_ON_IMPORT

KwMEASURE

KwDISPLAY

KwREWRITE

KwQuote

KwQuoteTerm

KwUnquote

KwUnquoteDecl

KwUnquoteDef

KwSyntax

KwPatternSyn

KwTactic

KwCATCHALL

KwVariable

KwNO_POSITIVITY_CHECK

KwPOLARITY

KwNO_UNIVERSE_CHECK

Instances

Show Keyword

Defined in Agda.Syntax.Parser.Tokens

Methods

showsPrec :: Int -> Keyword -> ShowS

show :: Keyword -> String

showList :: [Keyword] -> ShowS

Eq Keyword

Defined in Agda.Syntax.Parser.Tokens

Methods

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

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

layoutKeywords :: [Keyword]

Unconditional layout keywords.

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

data Symbol

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

Show Symbol

Defined in Agda.Syntax.Parser.Tokens

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

Eq Symbol

Defined in Agda.Syntax.Parser.Tokens

Methods

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

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