Lucas Franceschino
Lucas Franceschino
Done, there was another issue, but more recent, so I closed that other one.
Here are some notes about this issue. # Context We would like to be able to capture impl. expressions in quoted F* (or Coq, Lean, whatever.). Implementations have no names...
Ah, yeah, that will probably be fine indeed! I will play with it :) From our last conversation on that topic: I tried numerous ugly hacks to capture ambient generics,...
Still relevant, and related to #1135.
Still relevant
Ah, that's the common `grep` MacOS issues...
Still an issue I believe
The dependency `proc-macro-error` is gone since #1385, so that part is fixed. This is still relevant otherwise: - [ ] fixing the script for MacOS - [ ] improve the...
Still something we want!
Closing, we will address with the new core models design.