Beispielverwendungen von MSets in Coq

Question

MSets scheinen der Weg für OCaml-style endliche Mengen zu sein. Leider kann ich keine Beispielanwendungen finden. Wie kann ich einen leeren MSet oder einen Singleton MSet definieren? Wie kann ich Union zwei MSets zusammen?

Answer 1

ich ein einfaches Beispiel für endliche Mengen natürlicher Zahlen zeigen lassen:

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` *) 

Sie Coq.MSets.MSetInterface lesen können die Operationen und Spezifikationen MSet s bieten zu entdecken.