Skip to content

Commit cd21687

Browse files
authored
feat: simp debug trace tag to use “dpre” in rlfOnly mode (#5073)
to distinguish from `pre`.
1 parent a08ef5f commit cd21687

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Lean/Meta/Tactic/Simp/Rewrite.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -373,13 +373,13 @@ def rewritePost (rflOnly := false) : Simproc := fun e => do
373373

374374
def drewritePre : DSimproc := fun e => do
375375
for thms in (← getContext).simpTheorems do
376-
if let some r ← rewrite? e thms.pre thms.erased (tag := "pre") (rflOnly := true) then
376+
if let some r ← rewrite? e thms.pre thms.erased (tag := "dpre") (rflOnly := true) then
377377
return .visit r.expr
378378
return .continue
379379

380380
def drewritePost : DSimproc := fun e => do
381381
for thms in (← getContext).simpTheorems do
382-
if let some r ← rewrite? e thms.post thms.erased (tag := "post") (rflOnly := true) then
382+
if let some r ← rewrite? e thms.post thms.erased (tag := "dpost") (rflOnly := true) then
383383
return .visit r.expr
384384
return .continue
385385

0 commit comments

Comments
 (0)