From d364c8cdd600c75992811219ea690082e155f304 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 14 Feb 2024 19:56:42 -0500
Subject: [PATCH] chore: remove leftover `#check`s

---
 Alloy/Util/Parser.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Alloy/Util/Parser.lean b/Alloy/Util/Parser.lean
index a43128f..b6e19df 100644
--- a/Alloy/Util/Parser.lean
+++ b/Alloy/Util/Parser.lean
@@ -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.