Brent Yorgey

Note that there are now a bunch of good examples of using`prettyprinter` in https://github.com/swarm-game/swarm/ .

Abstractly, given the complete set of types $T$ which a term could have, we only want to display all the minimal ones with respect to subtyping. That is, if $\sigma,...

Closed by #365 .

#71 is related. In fact it seems like this might have worked correctly before https://github.com/disco-lang/disco/commit/5c4cdf15262a0765d4ae87ecfc813246ba6b2fc1 . We need both `2 f(n)` to parse as `2 * (f @ n)` and...

Could also make sense to split these two things into separate projects.

This is definitely not urgent and probably won't happen for a while, or until someone looking to make a big contribution picks it up.

What if there was a simple way to give "proof terms"? For example, we could define a proof term for `∀ n:N. ∃ m:N. f3(m) == n` as something like...

So maybe the thing to do here is to take a cue from the way we solved #17 and simply disallow shadowing in comprehensions. There's really no good reason to...

See https://github.com/disco-lang/disco/blob/474384f5682dcd2b94f0aae1a58c578f1639c6df/src/Disco/Enumerate.hs . The obvious thing we need to do is extend the `enumType` function to handle `TyUser`. However, in order to do that we would need to add an...

Thanks for the report! You're right that there's no reason we can't export `pFst` and `pSnd`, that was probably just an oversight. (Though really, perhaps we ought to now just...