Clément Pit-Claudel

Aliasing is the right solution, but it would indeed be nice if we did it by default. The problem here is that (IIRC) we can't define an alias between python-mode...

Hi there, Rupicola is still in exploratory stages at the moment; it's the spiritual successor to https://link.springer.com/chapter/10.1007%2F978-3-030-51054-1_7 , which used Facade and Bedrock 1 and was stuck on an old...

> A video call would be great; I would love to learn about the project; when would you have time for this? Super. Next week would be best for me....

> You spoke of a Mattermost channel that we could use to discuss rupicola related questions; would it be possible to add Benjamin, Bas and myself to this? Bas actually...

Yes, definitely I think: Bedrock 2 also has an unverified C backend. We haven't wired Rupicola to work with it yet.

Here are two arguments in favor of reporting `A.x`: - Extraction already reports it ```coq Require Import Extraction. Extraction M. ``` ``` Warning: The following axiom must be realized in...

> > Print Assumptions M.y. > > prints closed not A.x This one makes sense, right? > I think the more predictable behavior might be "Print Module Assumptions A is...

Fair point!

Any updates on this?

In the same vein, this is puzzling: ``` Fail Definition initial_value (v: test) : match v with | a => nat | b _ => nat end := match v...