Yes, this is where I am coming to as well!
Conversation
Meaning I was thinking it through today and feeling that I might need it on neutrals. I'm just unsure what happens during readback? Do variables get the lift back?
1
I've found it leads to wacky behavior like:
> let Id = Fun (A : Type) -> A -> A in Id^2
Fun (x0 : Type^2) -> (Fun (x1 : x0^4) -> x0^4) : Type^3
If I add it to the var constructor on neutrals
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
tis heartening to know I am not the only one
1
how does your naive version work? just brute force shift everything under binders?
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
Ahh, cool beans. Yeah, I think globals are stored as values in the internship report's one too, going off the repository. Part of my challenge has been figuring out how to do that with my current scheme, where I store things as values.
Here's the diff of the internship report: github.com/simhu/cubical/ - I find the environment structure a bit hard to grok though.
This Tweet was deleted by the Tweet author. Learn more
I've been trying to avoid globals because partly I want to try to head more towards something like 1ML, but perhaps that's a fool's effort. 😬
1
1
Show replies