Todd Wilson

One additional idea: when building the HTML, run abella with `witnesses=on` and use the information generated to enable display of search witnesses when hovering over the `search` tactic in a...

OK, thanks. As an aside, I noticed that this process only works if I copy all of my files to a directory in `abella/examples`; it doesn't work if I simply...

OK, then maybe instantiations are the wrong context for my suggestion. My primary concern was the following. When doing a `case` on a hypothesis of the form `{...}`, you get...

Thanks for the comment. I seem to remember getting weakening in situations other than with underscore arguments, but I guess I was mistaken. My sense is that allowing weakening, even...

I just wanted to add that I've come across many instances where it would be nice to be able to say that applying a theorem doesn't change the height of...

I anticipated the difficulty of getting useful information from the potentially overwhelming output to come out of a failed search in my initial comment, but my intuition is still that...

This is a very old but still open thread. I'm wondering whether another thought I've had a few times now might be relevant to the same aim. Often in a...

I'll add one more comment to this issue on the original suggestion, which I still think is good. One thing that I am often faced with in defining specification predicates...