MSets https://coq.inria.fr/library/Coq.MSets.MSets.html似乎是 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 https://coq.inria.fr/library/Coq.MSets.MSetInterface.html了解操作和规格MSets 提供。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
