Commit d7bf36da authored by Robbert Krebbers's avatar Robbert Krebbers

FromOp and IntoOp instances for frac.

parent 3875c726
Pipeline #4243 passed with stage
in 6 minutes and 48 seconds
From Coq.QArith Require Import Qcanon. From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra. From iris.algebra Require Export cmra.
From iris.proofmode Require Import classes.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Notation frac := Qp (only parsing). Notation frac := Qp (only parsing).
...@@ -48,3 +49,8 @@ Proof. done. Qed. ...@@ -48,3 +49,8 @@ Proof. done. Qed.
Lemma frac_valid' (p : Qp) : p (p 1%Qp)%Qc. Lemma frac_valid' (p : Qp) : p (p 1%Qp)%Qc.
Proof. done. Qed. 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
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