如何从多重集的所有元素中提取数据？

如何解决如何从多重集的所有元素中提取数据？

假设我有一个名为 dtyp 的数据类型。看起来像这样

datatype dtype = T bool int

我想定义一个函数 extr :: "dtype multiset => int multiset"，它接受​​这些 dtype 元素的多重集并返回一个包含每个 dtype 元素中的整数的多重集。例如：

value "extr {#T True 4,T False 5,T False 7#}" 应该给 {#4,5,7#}

我首先想到遍历多重集，但我知道这是不可能的，因为这些多重集基于不可迭代的普通集。然后我想到了全称量词，但我不确定在这种情况下如何使用它们。可以请我帮忙吗？

提前致谢！

解决方法

直接定义提取器的一些花哨的语法：

datatype dtype = T bool (payload: int)

考虑集合是一个很好的起点：您正在寻找 image 来表示多重集合。该函数存在，它被称为image_mset。所以：

definition extr :: "dtype multiset => int multiset" where
  "extr = image_mset payload"

image_mset 的语法 `# 尚未添加到 Multiset 条目中，但已被各种人使用。

notation image_mset (infixr "`#" 90)