From 204742bf2449c88abaea8ebd284c55d98b43488a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 14:48:08 +0200
Subject: Improve progress

---
 backends/lean/Base/Arith/Int.lean | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'backends/lean/Base/Arith')

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 5f00ab52..ac011998 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -32,14 +32,6 @@ instance (x y : Int) : PropHasImp (¬ x = y) where
 
 open Lean Lean.Elab Lean.Meta
 
--- Small utility: print all the declarations in the context
-elab "print_all_decls" : tactic => do
-  let ctx ← Lean.MonadLCtx.getLCtx
-  for decl in ← ctx.getDecls do
-    let ty ← Lean.Meta.inferType decl.toExpr
-    logInfo m!"{decl.toExpr} : {ty}"
-  pure ()
-
 -- Explore a term by decomposing the applications (we explore the applied
 -- functions and their arguments, but ignore lambdas, forall, etc. -
 -- should we go inside?).
-- 
cgit v1.2.3