diff options
| author | Son Ho | 2023-07-19 14:48:36 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-19 14:48:36 +0200 |
| commit | 753907aafc2502ced0cd8c3f9bc43fb1c4b30e93 (patch) | |
| tree | bcbe8537899de395b2f0391e07d05a4572734880 /backends | |
| parent | 204742bf2449c88abaea8ebd284c55d98b43488a (diff) | |
Cleanup a bit
Diffstat (limited to '')
| -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 |