Commit 8234670f authored by Robbert Krebbers's avatar Robbert Krebbers

Qp is inhabited.

parent b95c0bc7
......@@ -504,6 +504,8 @@ Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
Infix "/" := Qp_div : Qp_scope.
Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
Lemma Qp_eq x y : x = y Qp_car x = Qp_car y.
Proof.
split; [by intros ->|].
......
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