summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Utils.lean5
1 files changed, 0 insertions, 5 deletions
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