Owen Lynch
Owen Lynch
As discussed in private conversation, we want to strip out all of the renaming support here, because we have decided that renaming is tricky to get right. So this should...
There are actually *two* uses for renaming: renaming operations and renaming types. Of the two, I think that renaming operations is "more destructive". For instance, we would use renaming operations...
I'm happy not calling it Package, but I don't like namespace. The point is that `Package` doesn't just include the names; it also includes an assignment of those names to...
My thought is that we are going to use the multiple-inheritance branch instead of this, so this should not be merged, is that right @kris-brown?
This was addressed a while ago.
Waaaaaaat that would be so cool.
There's some stuff that's pretty special to GATs; I use the e-graph to perform type inference. That *might* be possible with metatheory metadata, but I'm not sure. E-Graphs are a...
I mean, idk about performant, but it's already *done* in Gatlab. At some point we will care about performance, but the focus now is less on hardcore term rewriting, and...
Thinking about this again. A single context in a theory is just a theory morphism out of the single-type theory. Thus, figuring out how to migrate theories along morphisms subsumes...