summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Progress/Progress.lean2
1 files changed, 0 insertions, 2 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 3b0248fe..9e2461a2 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -218,8 +218,6 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
-#check Environment
-#check ConstMap
def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
let args := args.raw
-- Process the arguments to retrieve the identifiers to use