feat: adaptations for leanprover/lean4#3210

leanprover-community / aesop

White-box automation for Lean 4

Apache License 2.0

191 stars 26 forks source link

feat: adaptations for leanprover/lean4#3210 #98

Closed kim-em closed 8 months ago

kim-em commented 8 months ago

These are adaptations for leanprover/lean4#3210.

[ ] depends on: https://github.com/leanprover/std4/pull/571

JLimperg commented 8 months ago

Looks good, feel free to merge this once the dependencies are merged.

Proper support for simprocs (which Aesop currently just ignores) will need broader changes, but I'll combine these with a refactoring of Aesop's simp integration.

kim-em commented 8 months ago

I'm going to merge this without updating the dependency, which I'll do tomorrow with the release.