Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: jdavis27@uiuc.edu
Hi,
The function map_add in HOL/Map.thy takes two partial
functions m1 and m2 and returns a partial function with the
mappings of m1 present in m2. Its infix notation is
m1++m2. Is there a subtractive version of the same
function? In other words, something like m1--m2 which
removes from m2 any mappings present in m1?
Thanks,
Justin S. Davis
Email Gateway (Aug 17 2022 at 13:27):From: Tjark Weber <tjark.weber@gmx.de>
Justin,
as far as I know there isn't, but what you want is easy to define
in terms of existing concepts:
constdefs
map_sub :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "--" 100)
"f--g == f |` (- dom g)"
Best regards,
Tjark
Last updated: May 03 2024 at 08:18 UTC