Commit f6f3b9c6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix prettty printing of multiset literals.

parent 03290b88
......@@ -938,10 +938,11 @@ Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
Class SingletonMS A B := singletonMS: A B.
Global Hint Mode SingletonMS - ! : typeclass_instances.
Instance: Params (@singletonMS) 3 := {}.
Notation "{[+ x +]}" := (singletonMS x) (at level 1) : stdpp_scope.
Notation "{[+ x +]}" := (singletonMS x)
(at level 1, format "{[+ x +]}") : stdpp_scope.
Notation "{[+ x ; y ; .. ; z +]}" :=
(disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
(at level 1) : stdpp_scope.
(at level 1, format "{[+ x ; y ; .. ; z +]}") : stdpp_scope.
Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
match mx with None => | Some x => {[ x ]} end.
......
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