James Wilcox

Thanks for the ideas! I'm looking forward to those patches being merged even more now.

Here's the generator (out of context) let rec expr_gen = lazy ( choose [ map [bytes] Syntax.STLC.var; map [bytes; ty_gen; unlazy expr_gen] @@ Syntax.STLC.lambda; map [unlazy expr_gen; unlazy expr_gen] @@...

Excellent, thanks! Would you be amenable to a PR that prints a warning if `size

Also, while I'm looking, what's the deal with this function that always returns false? https://github.com/stedolan/crowbar/blob/c8209e74aefe37cfdefc8fd4878e74426561c3ee/src/crowbar.ml#L237

I just had a chance to try this again with the fix of adding at least one constant inside the choose, but I still get stack overflows after a few...

I'll have to look more closely, but I think it's fair to say that this bug boils down to "UPDR does not support definitions", which we should fix.

Ah, on further review, this specific stack trace actually boils down to "mypyvy's evaluator for FOL formulas does not support definitions", which we should also fix :)

Yeah, we've been talking about doing definition expansion earlier in the pipeline for a while. (Currently definitions are only expanded at the very last second, during translation to Z3.) This...

We decided to remove the phase-automaton feature from the master branch because we were not planning to improve on our Phase-UPDR paper in the near future. Instead, we hope to...

I believe one of the concrete suggestions was something like ``` Require Import StructTact.StructTactics. Tactic Notation "find_rewrite" "