Literal Map syntax?

Stream: lean4

[Mac]

Is there any builtin Lean 4 syntax for creating literal Maps (ex. RBMap/HashMap) akin to JSON's record syntax (or Lean's own record syntax for structures)? If not, is this a possible future feature?

[Notification Bot]

Mac has marked this topic as resolved.

[Notification Bot]

Mac has marked this topic as unresolved.

[Mario Carneiro]

Nothing built in, but lean 3 has a syntax for this a la {a, b, c}, and it is not difficult to write something equivalent yourself