Is there some way to report error messages from inside Aesop, if I run a tactic and I know its failure means the rest of the search has to fail? I think if I fail out of a RuleTac it'll bury any error message in the search, but possibly there is a way out of that.
We could allow rules to report a 'fatal failure' which immediately terminates the search.
Geoffrey Irving asks on Zulip:
We could allow rules to report a 'fatal failure' which immediately terminates the search.