FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Forbid `//` in operators

Open W95Psp opened this issue 3 years ago • 0 comments
trafficstars

Hi,

As discussed last Monday, this PR, subsequent of #2666, changes the lexer so that the sequence // is forbidden in operators. The string ++//* used to be lexed as the operator ++//*, now it is lexed as the operator ++ and the comment //*.

W95Psp avatar Sep 02 '22 10:09 W95Psp