Skip to content
Snippets Groups Projects
Commit e29a5aee authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Literals 2, 3, and 4 for `Qp`.

parent 8fdeb77f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 1 deletion
theories/numbers.v
+ 4
− 1
View file @ e29a5aee
...@@ -541,11 +541,14 @@ Next Obligation. ...@@ -541,11 +541,14 @@ Next Obligation.
<-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r. <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed. Qed.
Notation "1" := Qp_one : Qp_scope.
Infix "+" := Qp_plus : Qp_scope. Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope. Infix "-" := Qp_minus : Qp_scope.
Infix "*" := Qp_mult : Qp_scope. Infix "*" := Qp_mult : Qp_scope.
Infix "/" := Qp_div : Qp_scope. Infix "/" := Qp_div : Qp_scope.
Notation "1" := Qp_one : Qp_scope.
Notation "2" := (1 + 1)%Qp : Qp_scope.
Notation "3" := (1 + 2)%Qp : Qp_scope.
Notation "4" := (1 + 3)%Qp : Qp_scope.
Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y. Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y.
Proof. Proof.
......
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