Geoffrey Irving

@darionco I also tried yours. I forget why it didn't work.

One specific desiderata: any call to `params_dict` should either throw an exception or return the same thing regardless of when it's called.

@ibab: @tomhennigan is already on this.

I'm hitting what I believe is the same problem, with ocaml 4.04 and camlp5 6.17: (master) beltrami:hol-light% camlp5 -v Camlp5 version 6.17 (ocaml 4.04.0) The full output of `make` is...

Actually Rob Arthan provided me with a patch that fixes the problem. It's attached, but a bit of work would have to be done before it could be safely integrated....

Thanks, I'll let you know if I come up with anything. For the moment I'm trying to avoid digging into parser algorithms as much as possible, though I may have...

Possibly this needs to wait on more general changes to implicit variables: https://github.com/leanprover/lean4/issues/2452.

Exciting!

Another example screenshot. Typically I search for something, it starts with lovely highlighting, and then the highlighting gets blurrier and blurrier as I edit until I clear the search. ![Weird...

@ludwigschubert Should we just close this one?