Jordan Mitchell Barrett (Apr 01 2021 at 10:49): Jordan Mitchell Barrett (Apr 01 2021 at 10:49):Suppose my current goal reads
(a,b) = (a0,b0)
Is there a tactic I can apply to discharge this goal, and generate two new goals:
a = a0
b = b0
?
More generally, if I have a type
Inductive foo :=
...
| bar : A0 -> A1 -> ... -> An -> foo
...
and a goal that reads
bar a0 a1 ... an = bar a'0 a'1 ... a'n
can I discharge this to the n+1 goals
a0 = a'0
a1 = a'1
...
an = a'n
?
Alix Trieu (Apr 01 2021 at 10:50):The f_equal tactic ?
Jordan Mitchell Barrett (Apr 01 2021 at 10:57):Works a charm, thanks!
Last updated: Oct 01 2023 at 19:01 UTC