Commit 4345aec5 authored by Robbert Krebbers's avatar Robbert Krebbers

Name some intro-ed stuff.

parent d6389a35
Pipeline #1259 passed with stage
......@@ -14,7 +14,7 @@ Instance frac_op : Op frac := λ x y, (x + y)%Qp.
Definition frac_ra_mixin : RAMixin frac.
Proof.
split; try apply _; try done.
unfold valid, op, frac_op, frac_valid. intros. trans (x+y)%Qp. 2:done.
unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
Qed.
Canonical Structure fracR := discreteR frac frac_ra_mixin.
......
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