summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2023-07-17 23:37:31 +0200
committerSon Ho2023-07-17 23:40:38 +0200
commit3e8060b5501ec83940a4309389a68898df26ebd0 (patch)
treeb02399a2137e8bbe54c181def92b5b43d5e42cf5 /backends/lean/Base/Progress
parent510e409b551f876a28f93f869e108f3f9e761212 (diff)
Reorganize the Lean backend
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Progress/Progress.lean2
1 files changed, 2 insertions, 0 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 35a3c25a..af7b426a 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -7,6 +7,7 @@ namespace Progress
open Lean Elab Term Meta Tactic
open Utils
+-- TODO: remove
namespace Test
open Primitives
@@ -199,6 +200,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
elab "progress" args:progressArgs : tactic =>
evalProgress args
+-- TODO: remove
namespace Test
open Primitives