James Wood
James Wood
Potential issue: opening a generated module will put names in scope depending on the result of a macro. This might cause difficulties for the scope checker.
There was no progress during AIM, as I was busy with other things. The proposal looks good to me. I imagine that if this issue ever gets acted upon, then...
Do you think it's worth adding a README file for the `Relation.Unary` combinators? Perhaps not, but I'm not sure how to learn them without reading one of your papers. In...
I haven't carefully read the above discussion, but maybe I have something relevant to add (now I've been summoned). Subsequent to working on the `Data.Vec.Functional` hierarchy, I've found that whenever...
Purple is variables.
I'd like to at least give it a once-over. Do you have any opinions on the things that should be in stdlib rather than here, and getting versions synced up,...
Also, I think we should eventually axiomatise all of the required properties about `List` and `_∈_`. The only challenge I see there is what to do about `prod`, `⟨_⟩Π`, and...
I suppose I'll need to rebase at some point to turn `Structure` into `Bundle`.
Thanks for the reminder. agda/agda-stdlib#1756 should now be ready, so after that gets merged I should be able to delete those parts from this PR.
Is there an existing definition of administrative normal form? I guess this would be the first thing to want.