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

fix: comments ending in --/

Browse source 
Fixes #1883
This commit is contained in:
Sebastian Ullrich 2022-11-25 10:31:01 +01:00
parent 39f2322f35
commit 42a080fae2
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Basic.lean
View file

@ -456,7 +456,7 @@ partial def finishCommentBlock (nesting : Nat) : ParserFn := fun c s =>
if nesting == 1 then s.next' input i h
else finishCommentBlock (nesting-1) c (s.next' input i h)
else
finishCommentBlock nesting c (s.next input i)
finishCommentBlock nesting c (s.setPos i)
else if curr == '/' then
if h : input.atEnd i then eoi s
else

3
tests/lean/run/1883.lean Normal file
View file

@ -0,0 +1,3 @@
/-- this docstring doesn't end with minus-slash as it should --/
def foo : Nat := 37