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



The code to lex string and character literals. Basically the same code as in GHC.



litString :: LexAction TokenSource

Lex a string literal. Assumes that a double quote has been lexed.

litChar :: LexAction TokenSource

Lex a character literal. Assumes that a single quote has been lexed. A character literal is lexed in exactly the same way as a string literal. Only before returning the token do we check that the lexed string is of length 1. This is maybe not the most efficient way of doing things, but on the other hand it will only be inefficient if there is a lexical error.