如何在Coq中創建合奏

Question

如何在Coq中創建一組元素？

我看過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.