Jon Sterling
Jon Sterling
@clayrat My guess is that it has to do with that issue I mentioned on IRC where you need some elim form to have the exact right boundary. Sorry I...
@favonia I'm not sure if it really should generate a warning, because the shape of the proof state is dynamic. But I'm not strongly against it either...
@favonia I guess I was thinking that one doesn't want a script to depend that sharply on the actual structure of the proof state, but now I think you're right...
I don't like this solution, because it actually requires elaborating it to not this lambda, but a type annotated one. This will disrupt overloading of constructors, so it is a...
(Sorry if my comment was difficult to understand, I am very sleepy. Will revisit tomorrow/today.)
I'll think about it agian when I'm more awake. it may be possible to do what you want without disrupting anything...
@favonia For some reason I'm worried about that idea, but I don't know why :laughing: I'll think it over.
@favonia If you are in a goal like `!- P x`, it changes the goal to `!- (x : A) -> P x`. This is used internally in the pattern...
@favonia Could you elaborate? I'm not sure. Thinking about it a bit more, I am not sure that hereditary substitutions scale up very well to the kind of thing we're...
@favonia the invariant is not broken if the user is writing programs interactively.