search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
191 stars 26 forks source link

Can't erase simprocs #113

Open JLimperg opened 7 months ago

JLimperg commented 7 months ago

MWE:

import Aesop

example : True := by
  simp [-Nat.reduceAdd]

example : True := by
  aesop (erase simp [Nat.reduceAdd])
  -- aesop: 'Nat.reduceAdd' is not registered (with the given features) in any rule set.

Nat.reduceAdd is a simproc.