Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Constrained.Spec.Set
Contents
Documentation
Constructors
SetSpec (Set a) (Specification a) (Specification Integer) |
guardSetSpec ∷ (HasSpec a, Ord a) ⇒ [String] → SetSpec a → Specification (Set a) Source #
data SetW (d ∷ [Type]) (r ∷ Type) where Source #
Constructors
SingletonW ∷ (HasSpec a, Ord a) ⇒ SetW '[a] (Set a) | |
UnionW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] (Set a) | |
SubsetW ∷ (HasSpec a, Ord a, HasSpec a) ⇒ SetW '[Set a, Set a] Bool | |
MemberW ∷ (HasSpec a, Ord a) ⇒ SetW '[a, Set a] Bool | |
DisjointW ∷ (HasSpec a, Ord a) ⇒ SetW '[Set a, Set a] Bool | |
FromListW ∷ (HasSpec a, Ord a) ⇒ SetW '[[a]] (Set a) |
Instances
Logic SetW Source # | |
Defined in Constrained.Spec.Set Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires SetW as b, HasSpec a) ⇒ SetW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ SetW dom rng → List Term dom → Evidence (AppRequires SetW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ SetW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). SetW dom Bool → List Term dom → [Pred] Source # | |
Semantics SetW Source # | |
Syntax SetW Source # | |
Show (SetW ds r) Source # | |
Eq (SetW dom rng) Source # | |
singletons ∷ [Set a] → [Set a] Source #