coq - 如何在 Coq 中创建 Ensemble

Question

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

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

谢谢。

Answer 1

如上所述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.