fix comment parsing

This commit is contained in:
2023-05-20 16:20:36 -07:00
parent 255e21f08a
commit ec3cf04db4
4 changed files with 5 additions and 4 deletions

View File

@@ -1,5 +1,5 @@
module Ex module Ex
-- comment
data Bool : Type where data Bool : Type where
True : Bool True : Bool
False : Bool False : Bool

View File

@@ -26,8 +26,8 @@ rawTokens : Tokenizer (Token Kind)
rawTokens rawTokens
= match (alpha <+> many identMore) checkKW = match (alpha <+> many identMore) checkKW
<|> match (some digit) (Tok Number) <|> match (some digit) (Tok Number)
<|> match (some opChar) (\s => Tok Oper s)
<|> match (lineComment (exact "--")) (Tok Space) <|> match (lineComment (exact "--")) (Tok Space)
<|> match (some opChar) (\s => Tok Oper s)
<|> match symbol (Tok Symbol) <|> match symbol (Tok Symbol)
<|> match spaces (Tok Space) <|> match spaces (Tok Space)

View File

@@ -12,6 +12,7 @@ public export
data Literal = LString String | LInt Int | LBool Bool data Literal = LString String | LInt Int | LBool Bool
public export public export
data RigCount = Rig0 | RigW data RigCount = Rig0 | RigW
-- I think I got Eq from pi-forall, it uses it for equality args (which are kinda like Prop/Rig0?)
public export public export
data Plicity = Implicit | Explicit | Eq data Plicity = Implicit | Explicit | Eq