Library Containers.MapNotations

Require Import MapInterface.

Notation "'[]'" := (empty _)(at level 0, no associativity) : map_scope.
Notation "M '[-' key '-]' " :=
  (find key M)(at level 31, left associativity) : map_scope.
Notation "M '[-' key '<-' v '-]' " :=
  (add key v M)(at level 29, left associativity) : map_scope.