Print goal when Aesop fails with `terminal := true` - Githubissues

leanprover-community / aesop

White-box automation for Lean 4

Apache License 2.0

192 stars 26 forks source link

Print goal when Aesop fails with `terminal := true` #47

Closed JLimperg closed 1 year ago

JLimperg commented 1 year ago

At the moment, we get a very uninformative error message.