From 69f032584e85c715641ee617578366c741e8f183 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 2 Nov 2023 18:14:28 +0100 Subject: [PATCH] fix constructor name in comment --- lib/Quox/Parser/Lexer.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr index eb71ad9..3780809 100644 --- a/lib/Quox/Parser/Lexer.idr +++ b/lib/Quox/Parser/Lexer.idr @@ -19,7 +19,7 @@ import Derive.Prelude ||| @ Reserved reserved token ||| @ Name name, possibly qualified ||| @ Nat nat literal -||| @ String string literal +||| @ Str string literal ||| @ Tag tag literal ||| @ TYPE "Type" or "★" with ascii nat directly after ||| @ Sup superscript or ^ number (displacement, or universe for ★)