Commit 173af5fb authored by Robbert Krebbers's avatar Robbert Krebbers

More documentation of f_equiv.

parent c9760e26
...@@ -250,11 +250,13 @@ Ltac setoid_subst := ...@@ -250,11 +250,13 @@ Ltac setoid_subst :=
| H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
end. end.
(** f_equiv works on goals of the form "f _ = f _", for any relation and any (** f_equiv works on goals of the form [f _ = f _], for any relation and any
number of arguments. It looks for an appropriate "Proper" instance, and applies number of arguments. It looks for an appropriate [Proper] instance, and applies
it. The tactic is somewhat limited, since it cannot be used to backtrack on it. The tactic is somewhat limited, since it cannot be used to backtrack on
the Proper instances that has been found. To that end, we try to ensure the the Proper instances that has been found. To that end, we try to ensure the
trivial instance in which the resulting goals have an [eq]. *) trivial instance in which the resulting goals have an [eq]. More generally,
when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
favor the second. *)
Ltac f_equiv := Ltac f_equiv :=
match goal with match goal with
| _ => reflexivity | _ => reflexivity
......
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