diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 8 |
1 files changed, 0 insertions, 8 deletions
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?). |