Skip to content
Snippets Groups Projects
Commit 5c98c9a8 authored by Ralf Jung's avatar Ralf Jung
Browse files

add Params

parent f3cc33ae
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/algebra/lib/dfrac_agree.v
+ 1
− 0
View file @ 5c98c9a8
...@@ -6,6 +6,7 @@ Definition dfrac_agreeR (A : ofe) : cmra := prodR dfracR (agreeR A). ...@@ -6,6 +6,7 @@ Definition dfrac_agreeR (A : ofe) : cmra := prodR dfracR (agreeR A).
Definition to_dfrac_agree {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A := Definition to_dfrac_agree {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A :=
(d, to_agree a). (d, to_agree a).
Global Instance: Params (@to_dfrac_agree) 2 := {}.
(** To make it easier to work with the [Qp] version of this, we also provide (** To make it easier to work with the [Qp] version of this, we also provide
[to_frac_agree] and appropriate lemmas. *) [to_frac_agree] and appropriate lemmas. *)
Definition to_frac_agree {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A := Definition to_frac_agree {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A :=
......
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