Commit 1e2d180b authored by Robbert Krebbers's avatar Robbert Krebbers

COFE on type with leibniz equality.

parent e760dfb5
......@@ -272,6 +272,8 @@ Section discrete_cofe.
End discrete_cofe.
Arguments discrete_cofeC _ {_ _}.
Definition leibniz_cofeC (A : Type) : cofeT := @discrete_cofeC A equivL _.
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
Arguments Later {_} _.
......
......@@ -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