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

chore(library/init/lean/parser/token): avoid tryView

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-29 14:30:28 +01:00
parent 21f1d231b8
commit 1a6a87d4e2
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/parser/token.lean
View file

@ -261,9 +261,9 @@ def number.Parser : Parser :=
lift $ try $ do {
it ← leftOver,
stx ← token,
some _ ← pure $ tryView number stx | error "" (DList.singleton "number") it,
pure stx
} <?> "number"
if stx.isOfKind number then pure stx
else error "" (DList.singleton "number") it
}
instance number.Parser.tokens : Parser.HasTokens (number.Parser : Parser) := default _
instance number.Parser.view : Parser.HasView number.View (number.Parser : Parser) :=