Skip to content

Commit

Permalink
chore: remove leftover #checks
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed Feb 15, 2024
1 parent 1a57c81 commit d364c8c
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions Alloy/Util/Parser.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,6 @@ namespace Alloy

open Lean Parser PrettyPrinter Formatter Parenthesizer

#check pushNone
#check many1

/--
The parser `many1Lookahead(p, pAhead)`, repeats `p` up to a final `pAhead`.
It is thus useful when `p` and `pAhead` overlap.
Expand Down

0 comments on commit d364c8c

Please sign in to comment.