summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2024-06-13 22:37:18 +0200
committerSon Ho2024-06-13 22:37:18 +0200
commitd5cf75a0f8209298ad85f46249f14d5c3a24faf6 (patch)
treec101e6bffaf474da394229fa4bda3147409577a0 /backends/lean
parentb3dd78ff4c8785b6ff9bce9927df90f8c78a9109 (diff)
Update the tests
Diffstat (limited to '')
-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