From d7bf36da7a92e38ec6432c7d424e344aee903a99 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Jun 2017 09:57:03 +0200
Subject: [PATCH] FromOp and IntoOp instances for frac.

---
 theories/algebra/frac.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index f9d36f3cd..7ee8e3c73 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,5 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
+From iris.proofmode Require Import classes.
 Set Default Proof Using "Type".
 
 Notation frac := Qp (only parsing).
@@ -48,3 +49,8 @@ Proof. done. Qed.
 
 Lemma frac_valid' (p : Qp) : ✓ p ↔ (p ≤ 1%Qp)%Qc.
 Proof. done. Qed.
+
+Global Instance frac_into_op q : IntoOp q (q/2)%Qp (q/2)%Qp.
+Proof. by rewrite /IntoOp frac_op' Qp_div_2. Qed.
+Global Instance frac_from_op q : FromOp q (q/2)%Qp (q/2)%Qp.
+Proof. by rewrite /FromOp frac_op' Qp_div_2. Qed.
\ No newline at end of file
-- 
GitLab