fact: Definition FiniteSetSpec : ADT FiniteSetSig := ADTRep (Ensemble W) { Def Constructor sEmpty (_ : unit) : rep := ret (Empty_set _), Def Method sAdd (xs : rep , x : W) : unit := ret (Add _ xs x, tt), Def Method sRemove (xs : rep , x : W) : unit := ret (Subtract _ xs x, tt), Def Method sIn (xs : rep , x : W) : bool := (b <- { b : bool | b = true <-> Ensembles.In _ xs x }; ret (xs, b)), Def Method sSize (xs : rep , _ : unit) : W := (n <- cardinal xs; ret (xs, n)) }.
imports: Coq.Sets.Ensembles Fiat.ADT.Core Fiat.Common.Ensembles Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.FiniteSetADTs.BedrockWord