Commit f1f45de3 authored by Robbert Krebbers's avatar Robbert Krebbers

COFE on type with leibniz equality.

parent cc10608d
......@@ -194,6 +194,8 @@ Ltac unfold_leibniz := repeat
setoid_rewrite <-(leibniz_equiv (A:=A))
end.
Definition equivL {A} : Equiv A := (=).
(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
......
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