fix: remove partially copied code comment (#5070)

2024-08-16 10:42:30 +02:00 · 2024-08-16 10:42:30 +02:00 · a08ef5ffa2
commit a08ef5ffa2
parent 53e6e99a29
1 changed files with 0 additions and 1 deletions
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@ -483,7 +483,6 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
        if i + 1 = eqns.size then 0 else 1
      else
        100 - i
-      -- We assign very low priority to equational le
      d ← SimpTheorems.addConst d eqn (prio := prio)
    /-
    Even if a function has equation theorems,