Mike Shulman
Mike Shulman
I think would be useful if the [installation documentation](https://agda.readthedocs.io/en/v2.6.2.2/getting-started/installation.html#installation-of-the-development-version) mentioned that it is also possible to install the development version of Agda with `cabal install` instead of `make install`, and...
Especially when working with terms that take a long time to typecheck (or to fail to typecheck), it would be convenient if agda-mode would show something indicating what it is...
Hi Andrew, In searching for a way to automatically translate LaTeX to WeBWorK problem files, I stumbled across your [tex.se question](https://tex.stackexchange.com/questions/19538/can-latex-be-persuaded-to-produce-text-output) which led me here. This project looks really neat,...
I expect the following code to give a “this pattern-matching is not exhaustive” error: ```ocaml type _ bar = | Flag : int bar | Other : 'a bar let...
In utop 2.13.1 for ocaml 5.1.0, entering ```ocaml type t = t;; ``` causes the program to freeze and become unresponsive, instead of giving the correct error message "The type...
I learned from Dan Doel [here](https://proofassistants.stackexchange.com/a/964) that the following definition is accepted: ```agda record Stream (A : Set) : Set where coinductive constructor _::_ field head : A tail :...
This is the third time I've wanted to ask this. The first two times, I found another way to do what I wanted, and maybe I would be able to...
`TODO insert call for papers` `TODO cover these topics: scope, submission format, selection procedure, notification, possibly also post-publication` `TODO submission information`
### Travel to Pittsburgh `TODO: information about travel to Pittsburgh` ### Venue `TODO: how to get to the venue once in Pittsburgh` ### Lodging `TODO: recommended hotels, or just point...
- better description (who is this for, what topics are covered, etc.) - explain financing support if any - explain application procedure - when ready: pointers to educational material and...