diff options
Diffstat (limited to 'backends/lean')
-rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 2 |
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 |