如何将所有列表或联合添加在地图中的所有图像中设置在Isabelle中
假设p是将映射定义为nat⇒字符串列表或nat⇀字符串列表，我想将P中的所有字符串列表附加
为类似的问题，如果P是定义为nat的地图⇒字符串集或nat⇀字符串SET，我想在P的图像中将所有字符串列表结合。
例如，对于p：0-＆gt; [“ 0.0”]; 1 - ＆GT; [“ 1.0”，“ 1,1”]，我想将结果作为[“ 0.0”，“ 1.0”，“ 1.1”]
for p：0 - ＆gt; {“ 0.0”}; 1 - ＆GT; {“ 1.0”，“ 1,1”}，我想将结果作为{“ 0.0”，“ 1.0”，“ 1.1”}，
看来Isabelle中有<代码>⋃要处理设置联合，但我找不到有关附加列表的任何信息。
Assume that p is a map defined as nat ⇒ string list or nat ⇀ string list and I want to append all string list in p's image
As the similar question, if p is a map defined as nat ⇒ string set or nat ⇀ string set and I want to union all string list in p's image.
For example, for p: 0 -> ["0.0"]; 1 -> ["1.0","1,1"], I want to get the result as ["0.0", "1.0", "1.1"]
for p: 0 -> {"0.0"}; 1 -> {"1.0","1,1"}, I want to get the result as {"0.0", "1.0", "1.1"}
It seems that in Isabelle has ⋃ to deal with the set union, but I can't find anything about append a set of lists.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论