Stream: Coq users

Topic: Tactic to change type of goal


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Callan McGill (Mar 02 2022 at 23:43):

Thank you as always!


Last updated: Jan 27 2023 at 01:03 UTC