Jacques Carette
Jacques Carette
We're also closing this one, for now, in favour of project issue #2511 as it's been hanging idle for too long and still requires a lot of work.
This is nice - but I wouldn't spend too much effort on it. When you have ~30 structures in your Algebra library, there's a limited number of natural diamonds that...
In my own projects (here on github), I've been using the wiki feature to make sure such discussion gets a more archival home. Another possibility is markdown files in the...
Basic issue: records and the current tools we have for declaring them are insufficient tools to help us represent theories and their relations adequately. Records are the low-level 'compilation' target...
That certainly would be an excellent start!
Definitely very interested. The next couple of days are very busy for me, but I'll give more detailed comments as soon as I can. (Others are most welcome to comment...
Turns out that "very busy" extended for *months*! I now have a nice 2 week window before the next term starts... I think the results in your first list seem...
Thanks. And no worries - all progress is good progress.
This looks good to me. I tried to find the second refactor on the branch you pointed to, but I wasn't quite sure what to look at (i.e. which commits...
> [...] does it make sense to aim to merge this in the meantime? As long as the additional refactor doesn't introduce compatibility issues, then yes, it makes sense to...