Jon Sterling
Jon Sterling
The mode is called `agda2-mode` (see https://agda.readthedocs.io/en/latest/tools/emacs-mode.html).
This might be a little hard, but I was having a look at the postscript backend (which looks very nice and useful), and it made me think that I could...
I am finding that for some reasons, certain lines of my code cause highlighting for the next several lines (or even the remainder of the file) to get disrupted; for...
Variant types in OCaml do not yet seem to be highlighted. It's not a big deal, but it would be nice to have!
Is there any reason to do this other than to get to use the `>>=` operator? I wonder if it makes things a little bit confusing... Perhaps defining an operator...
This is a draft PR containing @Trebor-Huang's work on exploring dcpo presentations, roughly following [Jung, Moshier, and Vickers](https://www.sciencedirect.com/science/article/pii/S1571066108004076). We will mark it as such when it is ready for review,...
Touches only sort of work when the device is rotated.
There is a remarkable idea from [Moegelberg](http://www.itu.dk/people/mogel/papers/lapl-fpc.pdf) that Lars Birkedal pointed out to me. Recall that it not the case that `EM(Lift) = Kleisli(Lift)` in the constructive setting (see #24);...
Developing this properties of this category, including its algebraic compactness (which remains conjectural in a constructive setting as far as I am concerned, but seems plausible) will be important for...