search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
157 stars 25 forks source link

Simp builder silently ignores rule penalty #62

Closed JLimperg closed 11 months ago

JLimperg commented 1 year ago

An attribute such as @[aesop norm simp 10] currently ignores the 10 and the simp lemma receives default priority. We should instead pass the priority along to the simplifier. Note that this priority has inverse semantics (higher is tried first, whereas for Aesop rules in general lower is tried first). Need to document this.

JLimperg commented 11 months ago

Fixed by the referenced commit.