leanprover-community / aesop

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

Support composite terms in local rules #110

Closed JLimperg closed 4 months ago

JLimperg commented 4 months ago

E.g. it should be possible to write (add ... (f x)) if f : Nat -> Prop and x : Nat are local hypotheses.