fix: use replay from leanprover/lean4#2617

leanprover-community / aesop

White-box automation for Lean 4

Apache License 2.0

192 stars 26 forks source link

Closed kim-em closed 11 months ago

kim-em commented 12 months ago

This is only relevant after leanprover/lean4#2617 is merged.

This PR uses Environment.replay instead of the playing-with-fire Environment.add which we would like to make private.

JLimperg commented 12 months ago

I'm really looking forward to getting rid of this hack. Thank you for your work on this!

kim-em commented 11 months ago

Closed, this was rolled into #71.