Kenji Maillard (Oct 29 2021 at 10:32): Kenji Maillard (Oct 29 2021 at 10:32):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
Gaëtan Gilbert (Oct 29 2021 at 10:34):classic bad relevance
it may be possible to get pose to generate correct relevance so worth an issue imo
Pierre-Marie Pédrot (Oct 29 2021 at 11:11):A way to print the relevances in debug mode would be appreciated btw.
Pierre-Marie Pédrot (Oct 29 2021 at 11:21):See https://github.com/coq/coq/pull/15090.
Pierre-Marie Pédrot (Oct 29 2021 at 11:21):Incidentally this fixes the issue I was mentioning last lunch with my descent into madness with prefascist CwFs
Kenji Maillard (Oct 29 2021 at 11:47):Filed an issue to keep track of this https://github.com/coq/coq/issues/15091
Last updated: Dec 01 2023 at 07:01 UTC