MSets
似乎是使用OCaml样式的有限集的方法。可悲的是,我找不到示例用法。
如何定义空的MSet
或单例MSet
?如何将两个MSets
合并在一起?
最佳答案
让我为有限的自然数展示一个简单的例子:
From Coq
Require Import MSets Arith.
(* We can make a set out of an ordered type *)
Module S := Make Nat_as_OT.
Definition test := S.union (S.singleton 42)
(S.empty).
(* membership *)
Compute S.mem 0 test. (* evaluates to `false` *)
Compute S.mem 42 test. (* evaluates to `true` *)
Compute S.is_empty test. (* evaluates to `false` *)
Compute S.is_empty S.empty. (* evaluates to `true` *)
您可以阅读
Coq.MSets.MSetInterface
来发现MSet
提供的操作和规范。关于set - Coq中MSets的示例用法,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/44793027/