How can we denote empty context in ltac1 while writing patterns for match
?
I wanted my tactic to apply simpl
when there are no hypotheses in the context.
How can that be done?
Doing [ |- _] => 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 simpl
?
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