Rodolphe Lepigre
Rodolphe Lepigre
Are we sure this is the right semantics? It seems to me that seeing toplevel commands like `Ltac2 Set` as things running only at "module initialization" (by analogy to OCaml's...
> Ocaml module initialization would be Require time not Import. That's why I put it in quotes, I agree the analogy is not perfect.
> I have no strong opinion about the expected semantics of Ltac2 late binding w.r.t. require / import. The new behaviour is more expressive than the previous one, and it's...
> Did you consider putting a flag on letin or lambda instead of using a constant? The difference would be for lambda `strict_fun x => body` (such that when applied...
> What is > > ``` > Eval lazy in ((unblock ((fun _ => block 42) tt))). > ``` > > supposed to produce? I would think `42` but I...
> > All constants should be universe polymorphic if they are not already > > Agreed. I hope the primitive mechanism allows for that. From what I remember it should...
I just pushed a rebase/cleanup, nothing new besides `let_lazy` being renamed into `run`.
@JasonGross this is indeed, true, but some rules are missing in the description. In particular, any progress made will be kept. So, the example you give will just be reduced...
I think that this can be unblocked with current dune by creating "dummy" theories for the various `elpi` folders. This requires changing the logical paths a bit, but that should...
I did manage to make things work with a flat directory structure based on something like the guide. However, I do want to preserve a directory structure in the generated...