Rivdo (Feb 26 2024 at 03:37): Rivdo (Feb 26 2024 at 03:37):During the proof, I have subgoals, is there any format that can apply the current tactic to the specified subgoals , or not prove the subgoals in the order they are parsed by the prover? Thanks in advance.
Yong Kiam (Feb 26 2024 at 03:40):defer n and prefer n shuffle the list of pending goals: defer puts off sub-
goal n to the end of the list (n = 1 by default), while prefer brings
sub-goal n to the front.
Last updated: Apr 27 2024 at 16:16 UTC