Syntax for creating concrete HashMaps

[austinletson]

In reviewing documentation examples for HashMap, @digama0 mentioned that it would be nice to have syntax for constructing concrete HashMaps.

The proposed syntax is {"one" ↦ 2, "two" ↦ 2} => HashMap.ofList [("one", 1), ("two", 2)].

[somombo]

I propose, #{"one" : 1, "two" : 2}

[Shreyas4991]

@digama0 also gave the syntax invocations to accomplish this. Posted below for completeness:

import Std

def Std.HashMap.ofList' [BEq α] [Hashable α] (l : List (α × β)) : HashMap α β := .ofList l

open Lean
syntax kvPair := term ": " term
syntax "!{" (term ": " term),* "}" : term
macro_rules | `(!{$[$k : $v],*}) => `(Std.HashMap.ofList' [$[($k, $v)],*])

#eval !{1: 2, 3: 4}.contains 1