Commit 58e2c608 authored by Robbert Krebbers's avatar Robbert Krebbers

Add `f_equiv/=` which performs `simpl` first.

This is similar to `f_equal/=`.
parent 30f481c2
Pipeline #5299 passed with stages
in 6 minutes and 32 seconds
...@@ -319,6 +319,7 @@ Ltac f_equiv := ...@@ -319,6 +319,7 @@ Ltac f_equiv :=
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
end; end;
try simple apply reflexivity. try simple apply reflexivity.
Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
(* The tactic [solve_proper_unfold] unfolds the first head symbol, so that (* The tactic [solve_proper_unfold] unfolds the first head symbol, so that
we proceed by repeatedly using [f_equiv]. *) we proceed by repeatedly using [f_equiv]. *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment