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

【问题标题】：How can I extract data from all elements of a multiset?如何从多重集的所有元素中提取数据？
【发布时间】：2021-04-28 23:04:06
【问题描述】：

假设我有一个名为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#}

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

提前致谢！

【问题讨论】：

【解决方案1】：

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

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)

【讨论】：