Commit 5912d750 authored by Robbert's avatar Robbert

Merge branch 'robbert/bind_notation' into 'master'

Pattern matching notation for monadic binds

See merge request robbertkrebbers/coq-stdpp!18
parents 5dc4837b dcd59f13
Pipeline #5512 passed with stages
in 4 minutes and 36 seconds
......@@ -887,25 +887,14 @@ Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 100, only parsing, right associativity) : stdpp_scope.
(at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.
Notation "' x1 .. xn ← y ; z" := (y = (λ x1, .. (λ xn, z) .. ))
(at level 20, x1 binder, xn binder, y at level 100, z at level 200,
only parsing, right associativity) : stdpp_scope.
Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
Notation "' ( x1 , x2 ) ← y ; z" :=
(y = (λ x : _, let ' (x1, x2) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "x ;; z" := (x = λ _, z)
(at level 100, z at level 200, only parsing, right associativity): stdpp_scope.
......@@ -918,9 +907,9 @@ Class MGuard (M : Type → Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
Arguments mguard _ _ _ !_ _ _ / : assert.
Notation "'guard' P ; z" := (mguard P (λ _, z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
(at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
(at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
(at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
(** * Operations on maps *)
(** In this section we define operational type classes for the operations
......
......@@ -27,7 +27,7 @@ Section definitions.
multiplicity x X multiplicity x Y.
Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
let (X) := X in '(x,n) map_to_list X; replicate (S n) x.
let (X) := X in ''(x,n) map_to_list X; replicate (S n) x.
Global Instance gmultiset_size : Size (gmultiset A) := length elements.
Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
......
......@@ -534,11 +534,12 @@ Definition Qp_minus (x y : Qp) : option Qp :=
match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end.
Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _.
Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed.
Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / ('y)%Z) _.
Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
Next Obligation.
intros x y. assert (0 < ('y)%Z)%Qc.
{ apply (Z2Qc_inj_lt 0%Z (' y)), Pos2Z.is_pos. }
by rewrite (Qcmult_lt_mono_pos_r _ _ ('y)%Z), Qcmult_0_l,
intros x y. assert (0 < Zpos y)%Qc.
{ apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
<-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.
......
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