I stumbled upon a strange interaction of pose with change on an inductive in SProp:
Inductive P : SProp := C. Goal forall (f : P -> Type) (x : P), f x. intros f x. (* Works as expected *) Fail Fail change x with C. pose (t := C). (* Does not work ??? *) Fail change x with t. (* Works if we explicitly unfold *) let tu := eval unfold t in t in change x with tu.
I am not sure were the problem is coming from and I didn't find a corresponding issue on github, should I open one ?
cc @Gaëtan Gilbert
classic bad relevance
it may be possible to get pose to generate correct relevance so worth an issue imo
A way to print the relevances in debug mode would be appreciated btw.
Incidentally this fixes the issue I was mentioning last lunch with my descent into madness with prefascist CwFs
Filed an issue to keep track of this https://github.com/coq/coq/issues/15091
Last updated: May 28 2023 at 16:30 UTC