max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: naming convention

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-19 10:20:42 -07:00
parent 6c8322d20a
commit bdb2e9597a
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/lex.lean
View file

@ -20,7 +20,7 @@ inductive LexErr where
| notDigit : Char → LexErr
deriving Repr
def charDigit (char : Char) : Option Nat :=
def charDigit? (char : Char) : Option Nat :=
if char.isDigit then
some char.toNat
else
@ -34,7 +34,7 @@ mutual
| ')' => return { text := ")", tok := Tok.rpar } :: (← lex it.next)
| '+' => return { text := "+", tok := Tok.plus } :: (← lex it.next)
| other =>
match charDigit other with
match charDigit? other with
| none => throw <| LexErr.unexpected other
| some d => lexnumber d [other] it.next
else
@ -43,7 +43,7 @@ mutual
def lexnumber [Monad m] [MonadExceptOf LexErr m] (soFar : Nat) (text : List Char) (it : String.Iterator) : m (List Token) :=
if it.hasNext then
let c := it.curr
match charDigit c with
match charDigit? c with
| none => return { text := text.reverse.asString, tok := Tok.num soFar } :: (← lex it)
| some d => lexnumber (soFar * 10 + d) (c :: text) it.next
else