Commit 5c3c460e authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp

parents b26e5a4a 76b66f20
Pipeline #31513 passed with stage
in 12 minutes and 9 seconds
...@@ -35,6 +35,8 @@ sarahzrf, and Tej Chajed. ...@@ -35,6 +35,8 @@ sarahzrf, and Tej Chajed.
as integers `Z`, in analogy with `encode_nat`/`decode_nat`. as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
- Fix list `Datatypes.length` and string `strings.length` shadowing (`length` - Fix list `Datatypes.length` and string `strings.length` shadowing (`length`
should now always be `Datatypes.length`). should now always be `Datatypes.length`).
- Change the notation for pattern matching monadic bind into `'pat ← x; y`. It
was `''pat ← x; y` (with double `'`) due to a shortcoming of Coq ≤8.7.
## std++ 1.3 (released 2020-03-18) ## std++ 1.3 (released 2020-03-18)
......
...@@ -1046,9 +1046,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope. ...@@ -1046,9 +1046,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z)) Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 20, y at level 100, z at level 200, only parsing) : 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) .. )) Notation "' x ← y ; z" := (y = (λ x : _, z))
(at level 20, x1 binder, xn binder, y at level 100, z at level 200, (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.
only parsing, right associativity) : stdpp_scope.
Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope. Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
......
...@@ -28,7 +28,7 @@ Section definitions. ...@@ -28,7 +28,7 @@ Section definitions.
multiplicity x X = multiplicity x Y. multiplicity x X = multiplicity x Y.
Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X, 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_size : Size (gmultiset A) := length elements.
Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet . Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
......
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