Can I use "set" or something similar to match on a term of a given type in the goal? For example, say that my goal contains a subterm t of type bool, can I do something like "set z : bool := _ " or similar to set z := t?
Goal 1 = 1 /\ true = true. set (some_bool := _ : bool). (* some_bool := (true : bool) : bool |- 1 = 1 /\ some_bool = some_bool *) (* cbv beta will get rid of the extra cast with usually no or little reduction *) cbv beta in some_bool.
Nice, thank you!
Patrick Nicodemus has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC