Coq 中 MSet 的使用示例
Example uses of MSets in Coq
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
提供的操作和规范。
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
提供的操作和规范。