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
Conversation
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.
1
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. 😬
I think one of the issues with how I'm shifting neutrals (by putting it as a shift on the var constructor) is that I don't know whether to either accumulate the shift, or forget about it. In the NbE rules given in the thesis they don't shift through variables.
1
s/thesis/report/
1
Show replies