Re: [isabelle] Subtractive version of map_add



Justin,

On Thursday 20 October 2005 15:49, jdavis27 at uiuc.edu wrote:
> 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?

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.