Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nice representation for access to maps

view this post on Zulip Email Gateway (Aug 19 2022 at 08:10):

From: Peter Lammich <lammich@in.tum.de>
Hi

On maps, you have "dom" and "ran", that are the domain and range of the
map.

In your case, you could write: "ALL y\<in>ran mymap. P y"

view this post on Zulip Email Gateway (Aug 19 2022 at 08:10):

From: Brian Huffman <huffman@in.tum.de>
There is also the function Option.set :: 'a option => 'a set, which
may be useful:

ALL y\<in>Option.set (mymap i). P y

Last updated: Apr 25 2024 at 08:20 UTC