From d5cf75a0f8209298ad85f46249f14d5c3a24faf6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:37:18 +0200
Subject: Update the tests

---
 backends/lean/Base/Utils.lean | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 7225d8a3..5954f048 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -704,11 +704,6 @@ inductive Location where
   /-- Same as Tactic.Location -/
   | targets (hypotheses : Array Syntax) (type : Bool)
 
-#check Tactic.simpLocation
-#check Tactic.Location
-#check MVarId.getNondepPropHyps
-#check simpLocation
-
 -- Adapted from Tactic.simpLocation
 def customSimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none)
   (loc : Location) : TacticM Simp.Stats := do
-- 
cgit v1.2.3