Stream: Beginner Questions

Topic: Is there a particular syntax for Maps of a single element?

view this post on Zulip Hernán Rajchert (Feb 01 2023 at 20:23):

Hi, I'm working with Maps, and I noticed there is special syntax for updating a map, but I wasn't able to find how to create maps of a single element.

Is there a particular syntax to write this?

definition singleMap :: "'a ⇒ 'b ⇒ 'a ⇀ 'b" where
  "singleMap k v = (λx. if x = k then Some v else None)"

view this post on Zulip Mathias Fleury (Feb 01 2023 at 20:28):

Map.empty

view this post on Zulip Mathias Fleury (Feb 01 2023 at 20:30):

and updating that with the one element?

view this post on Zulip Hernán Rajchert (Feb 01 2023 at 20:49):

I thought of that, but I was wondering if there was a special syntax to avoid doing Map.empty (k ↦ v)

view this post on Zulip Manuel Eberl (Feb 01 2023 at 21:41):

You mean like this?

term "[1 ↦ 2, 2 ↦ 3]"

view this post on Zulip Hernán Rajchert (Feb 01 2023 at 22:06):

Thanks! that is exactly it... I just figured it out by having a nitpicked lemma :sweat_smile: Screen-Shot-2023-02-01-at-19.05.25.png

Last updated: Apr 26 2024 at 12:28 UTC