Callan McGill (Mar 02 2022 at 23:34): Callan McGill (Mar 02 2022 at 23:34):A bit of a vague question but is there a tactic where I can pass in a type or prop and that gives me two new subgoals one to prove that the type/prop implies my current goal and the second to prove the claimed thing?
Paolo Giarrusso (Mar 02 2022 at 23:39):enough P. Or the more common assert P, which gives the same goals but in the other order: first prove P, then use P in the original goal.
Callan McGill (Mar 02 2022 at 23:43):Thank you as always!
Last updated: Apr 19 2024 at 22:01 UTC