JLimperg
commented
3 months ago There's no conceptual reason, it's just a bunch of engineering effort. This features has been requested a few times and I'd also like to have it, so it's definitely going to happen at some point, hopefully soonish.
I recently found out about aesop and I think it is a really nice tool. But I have one question, why does aesop? not work on proofs that aren't fully completed by aesop? Is there a specific reason for this? Because sometimes aesop does some really useful things, which help a lot but don't close the proof completely. In these cases, it would be very nice to know what aesop did.