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

Merge branch 'bind-pattern-notation' into 'master'

Fix #70: add pattern variant of bind notation

Closes #70

See merge request !169
parents ab7ed0b8 f4718436
No related branches found
No related tags found
1 merge request!169Fix #70: add pattern variant of bind notation
Pipeline #31479 passed
......@@ -1046,9 +1046,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y ≫= (λ x : _, z))
(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.
Notation "' x ← y ; z" := (y ≫= (λ x : _, z))
(at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.
Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
......
......@@ -28,7 +28,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 ∅.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment