From 01148d8193ee97b365253d8cf7f457f4c5754c30 Mon Sep 17 00:00:00 2001 From: Sean Sube Date: Wed, 28 Sep 2022 17:34:13 -0500 Subject: [PATCH] use a char list for operators --- Parse.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Parse.agda b/Parse.agda index e878100..0aa17df 100644 --- a/Parse.agda +++ b/Parse.agda @@ -34,6 +34,9 @@ takeCons cs (x ∷ xs) with (findCharIndex 0 x cs) digits : List Char digits = primStringToList "0123456789" +opers : List Char +opers = primStringToList "=+" + -- parse a single character into a typed token parseChar : Char → Token parseChar '0' = Digit 0 @@ -68,7 +71,7 @@ takeNat s with takeCons digits s ... | emit (just n) rem₂ = emit (just n) rem₁ takeOper : List Char → Result Token -takeOper s with takeCons ('+' ∷ []) s +takeOper s with takeCons opers s ... | emit nothing rem = emit nothing rem ... | emit (just []) rem = emit nothing rem ... | emit (just (x ∷ xs)) rem with parseChar x