One can ask destruct to leave an equality between the original term and the destructed one using eqn:
. I am destructing a variable of record type in a dependent context. It would be useful if instead of an equation a = {| ... |}
I would get a definition a: = {| ... |}
so that a
and the destructed record are definitionally equal. I could switch between the two in the dependent context then using change
. I can find ways of doing this in non dependent cases, but non which work in a context where a
is used in a dependent context.
Last updated: Oct 13 2024 at 01:02 UTC