Stream: Coq users

Topic: destruct leaving a definition instead of an equality


view this post on Zulip Michael Soegtrop (May 03 2024 at 12:59):

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