How can we denote empty context in ltac1 while writing patterns for
I wanted my tactic to apply
simpl when there are no hypotheses in the context.
How can that be done?
[ |- _] => auto seems to match for any number of hypotheses. How can we restrict it to zero number of hypotheses?
Ltac foo := match goal with | [ |- _ ] => simpl end.
Maybe have a branch that matches on a hypothesis and fails?
So have a branch like
_ |- _ , check if it fails and then do
If that's so, how can we check failure on branch match? It will just go to the next branch, right?
Goal True -> 1 + 1 = 2. Proof. intros H. match goal with | _ : _ |- _ => idtac | _ => simpl end. (* goal: H : True |- 1 + 1 = 2 *) clear H. match goal with | _ : _ |- _ => idtac | _ => simpl end. (* goal: |- 2 = 2 *)
Got it, thanks.
Julin S has marked this topic as resolved.
Last updated: Oct 01 2023 at 19:01 UTC