coq - 如何在 Coq 中创建集成

如何在 Coq 中创建一组元素？

我已经查看了 Ensembles 的文档，但我没有看到任何构建它的方法。例如，在 Haskell 中，我会使用“Data.Set.fromList [1..10]”来创建一个包含 10 个元素的集合。 Coq 中的等价物是什么？

谢谢。

最佳答案

正如 here 所解释的，例如，您可以执行以下操作

Require Import List Ensembles.

Fixpoint list_to_set {A:Type} (l : list A) {struct l}: Ensemble A :=
  match l with
    | nil => Empty_set A
    | hd :: tl => Add A (list_to_set tl) hd
  end.

关于coq - 如何在 Coq 中创建集成，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/22353508/