Jacques Carette
Jacques Carette
I've been of the opinion for quite some time that things like `_≟_` should be in their own modules -- explicitly because of dependency issues. `Data.Nat.Properties` pulls in a *lot*...
We went a bit lens crazy, long ago. As to your fundamental question: no, we never want *change* that field. So changing it to a pure getter would be a...
We do seem to be talking past each other. I see the 'writeability' as being only an issue wrt to *changing* a UID of an existing chunk. You never want...
We should look at all the times we attempt to modify an existing chunk - I'm guessing all of those are, in our current design, a mistake. In other words,...
Commenting starting at: > I noticed that we have many areas where there is a list containing empty lists, which does cause issues when compiling because the code comprehends a...
Feels like there should be some kind of `init` process for the various processors that would load up the chunk database with their own "stuff". A good process would have...
Agda will have the best engineered library of them all! (I mean that).
That's how it was meant. What I really want to do next is to emulate (the good parts of) Kevin Buzzard and put as many students on implementing things as...
I've self-assigned this one. I think I can reconstruct an explanation for it all, with no promises that it's going to be coherent.
But I can 'answer' the aspect of this related to the title: `SystemInformation` tries to be *representation independent*. So instead of giving a type for each of its fields, it...