Carlo Angiuli

I think that's right -- it would help future automation if we knew that this particular opaque lemma is hcom. It would also be desirable to allow it to unfold...

Actually, there is one really important aspect of this design that I've only just edited into the issue description (sorry about that! lol), and it's that the created symbol should...

Yes, let's do it! When I was working on the recursive case some months ago, my thought was to immediately left-invert these new equations, i.e. to have an operation in...

What I like about this approach is that we don't need to bind and possibly even export two names for every operation like `symm` and `symm-filler`. But both ideas just...

After discussing with @jonsterling, we agreed that the best way to implement this feature is to build on #179. Suppose we define `symm` as an hcom 0->1 using the abstract...

I think it would be nice to expose some sort of `Eval Foo.` (for non-stable closed-term evaluation) and `Reduce Foo.` (for stable reduction under binders) at the top level. Currently...

Can you elaborate on (3)? How does that situation arise?

@favonia This shouldn't be too hard, right? I would like to have this so I can try to finish the vproj-is-an-equivalence proof in RedPRL. As it is, there are not...

Do you mean, types satisfying regularity? I thought we didn't think this was a useful kind.

Ah, I see. I have never thought seriously about their proof theory, and I don't think @mortberg has either?