fix some comments
This commit is contained in:
parent
da3cd404f3
commit
6c8ebfb804
1 changed files with 2 additions and 2 deletions
|
@ -163,7 +163,7 @@ private %inline
|
|||
supToNat : String -> Nat
|
||||
supToNat = cast . pack . map fromSup . unpack
|
||||
|
||||
-- ★0, Type0. base ★/Type is a Reserved
|
||||
-- ★0, Type0. base ★/Type is a Reserved and ★¹/Type¹ are sequences of two tokens
|
||||
private
|
||||
universe : Tokenizer ExtToken
|
||||
universe = universeWith "★" <|> universeWith "Type" where
|
||||
|
@ -312,7 +312,7 @@ tokens = choice $
|
|||
map skip [pred isWhitespace,
|
||||
lineComment (exact "--" <+> reject symCont),
|
||||
blockComment (exact "{-") (exact "-}")] <+>
|
||||
[universe] <+> -- ★ᵢ takes precedence over bare ★
|
||||
[universe] <+> -- Type<i> takes precedence over bare Type
|
||||
map resTokenizer reserved <+>
|
||||
[sup, nat, string, tag, name]
|
||||
|
||||
|
|
Loading…
Reference in a new issue