Jon Sterling
Jon Sterling
If it is indeed possible, this would be **_amazing**_! It might allow us to adopt MLton for all of [sml-red-jonprl](https://github.com/JonPRL/sml-red-jonprl), without having to support SML/NJ builds for development.
You may be interested in checking out what we did in cooltt, which is similar to your proposal i think.
What I mean is that in addition to supporting the `Sub`/`Ext` (pre)types, both `cooltt` and `redtt` keep the boundary constraint in the judgment as long as possible; it's true that...
Can you please make this code self-contained so that I can copy-paste it into Emacs?
Very nicely done @plt-amy! For the benefit of the Agda devs, let me comment a bit on how `cooltt`/`redtt` were carefully designed to avoid failures of subject reduction like this....
could it be caused by #288 ? LOL
Oh yeah, and something I should add is that one of the reasons I was interested in weak universes was that I was very concerned at the time about (1)...
I feel having the previous patches in scope is unexpected behavior from a user's point of view...
Just for fun, here's some example code that we could write if the above existed: ``` axiom syn : prop axiom tp : {syn} type axiom tm : {syn} tp...
I think the one place where we need some special feature it make the coherence with between an abstract hcom and something else. Am I missing something?