Brent Yorgey

``` type T(a) = Unit + a * T(a) * T(a) !!! forall t : T(N). mirror(mirror(t)) == t mirror : T(a) -> T(a) mirror(left(unit)) = left(unit) mirror(right(a,l,r)) = right(a,...

OK, but note to make this work, `enumerate` also has to handle user-defined types!

``` +isSearchable :: TyDefCtx -> Type -> Bool +isSearchable tyDefs = go S.empty + where + go :: Set (String, [Type]) -> Type -> Bool + go _ TyProp =...

Above is the code for `isSearchable`. Putting this off for now because getting `enumerate` to handle user-defined types is a bit tricky. First of all, we have to be able...

Using fixpoints sounds nice and tidy, but it would require some work when parsing type definitions: we would have to do some analysis to figure out mutually recursive groups of...

Creating files with comments and code in it, with definitions to be filled in by the user (with accompanying properties) seems to work well.

The reference documentation helps somewhat. But after this semester is over, I should start extracting exercises from some of the Discrete assignments I have made (+ creating more), with the...

Note, if we're going to have to put `...` sometimes anyway, then maybe we shouldn't worry about having the output be valid Disco syntax? As a crazy alternative idea, what...

As a much simpler alternative, if we're not worrying about having valid Disco syntax, then we might as well go all the way to something like ``` true -> false...

Here's a nice example of separating out lexing and parsing phases using megaparsec: https://gist.github.com/LightAndLight/36926a4e3a7133910d9aa199da50c4fd