Email Gateway (Aug 19 2022 at 08:10): Email Gateway (Aug 19 2022 at 08:10):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I have a map which maps type X to type Y option
type_synonym MAP = "X ⇒ Y option"
Given i is my index into the map:
i::X
I want to evaluate a proposition P about the map elements:
Proposition P :: Y -> bool
I only care about the map elements which exist, e.g. are not None:
ALL (y::Y). (mymap :: MAP) i = Some y ⟶ P y
Is there a way to get a nicer and more intuitive notation like:
P mymap[i]
Regards
Cornelius
Last updated: Nov 21 2024 at 12:39 UTC