本文介绍了Coq中MSets的示例用法的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
似乎是使用OCaml风格的有限集的方法。可悲的是，我找不到示例用法。
MSets appear to be the way to go for OCaml-style finite sets. Sadly, I can't find example uses.
如何定义空的 MSet 或单例 MSet ？如何将两个 MSets 结合在一起？
How can I define an empty MSet or a singleton MSet? How can I union two MSets together?
推荐答案
让我展示一个有限自然数集的简单示例：
Let me show a simple example for finite sets of natural numbers:
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` *)
您可以阅读来发现操作和规格提供 MSet 。
这篇关于Coq中MSets的示例用法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！