Jon Sterling
Jon Sterling
Hmm, I don't yet see why `deftype` addresses the way that we can't have records with fields of type `I->A`. Can you an example?
What I meant was, can I have an example of how your proposed `deftype` helps with this?
Oh I see. I’m ok with it > On Jun 24, 2022, at 2:02 PM, Reed Mullanix ***@***.***> wrote: > > > Sorry, misunderstood your request! > > With...
I think this is actually not too far beyond what I know how to do. Semantically `tp \ phi` is the collection of types `A` equipped with a _unique_ element...
There is a typo in the spec! The point p should be under phi. Then the empty type is 0=1-connected: the p is the unique map from 0=1 to the...
I've been studying Ulf Norell's thesis, and I think I see how to do a better job, which combines the main part of the unification algorithm and the conversion checker.
I see, thank you for the info! I briefly checked out the `.messages` stuff and it seems pretty neat; I wasn't able to figure out how to unleash it with...
We will hopefully be able to address this once we have a worked out theory of computational equivalence.
@kaonn Thanks for reporting this! I'm sorry that it's taking me a little longer than anticipated to look into it. Unfortunately, unleashing a couple of papers has been taking precedence...
I finally got around to looking at this, and it is unfortunate that it is happening so deep into a proof library that takes several minutes to typecheck. I am...