FilterV f k v ([] (Mapping Symbol *)) | |
|
(Conder ((||) ((==) Ordering (Cmp (Mapping Symbol *) x ((:->) Symbol * k v)) GT) ((==) Ordering (Cmp (Mapping Symbol *) x ((:->) Symbol * k v)) EQ)), FilterV FMax k v xs) => FilterV FMax k v ((:) (Mapping Symbol *) x xs) | |
|
(Conder ((==) Ordering (Cmp (Mapping Symbol *) x ((:->) Symbol * k v)) LT), FilterV FMin k v xs) => FilterV FMin k v ((:) (Mapping Symbol *) x xs) | |
|
Updatable v t ([] (Mapping Symbol *)) ((:) (Mapping Symbol *) ((:->) Symbol * v t) ([] (Mapping Symbol *))) | |
|
IsMember v t ((:) (Mapping Symbol *) ((:->) Symbol * v t) m) | |
|
IsMember v t m => IsMember v t ((:) (Mapping Symbol *) x m) | |
|
Updatable v t ((:) (Mapping Symbol *) ((:->) Symbol * v s) m) ((:) (Mapping Symbol *) ((:->) Symbol * v t) m) | |
|
Updatable v t m n => Updatable v t ((:) (Mapping Symbol *) ((:->) Symbol * w y) m) ((:) (Mapping Symbol *) ((:->) Symbol * w y) n) | |
|
Submap s t => Submap s ((:) (Mapping Symbol *) x t) | |
|
Split s t st => Split s ((:) (Mapping Symbol *) x t) ((:) (Mapping Symbol *) x st) | |
|
(KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) | |
|
Eq (Map ([] (Mapping Symbol *))) | |
|
(KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) | |
|
Show (Map ([] (Mapping Symbol *))) | |
|
(KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) | |
|
Show' (Map ([] (Mapping Symbol *))) | |
|
Sortable ([] (Mapping Symbol *)) | |
|
Nubable ([] (Mapping Symbol *)) | |
|
CoeffectZip [Mapping Symbol *] IxCoreader Source # | |
|
Coeffect [Mapping Symbol *] IxCoreader Source # | |
|
Effect [Mapping Symbol *] Reader Source # | |
|
Effect [Mapping Symbol *] Writer Source # | |
|
Submap s t => Subeffect [Mapping Symbol *] Reader s t Source # | If s is a subset of t then, s is a subeffect of t |
|
Supermap s t => Subeffect [Mapping Symbol *] Writer s t Source # | |
|
Submap ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) | |
|
Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) | |
|
(Sortable (Filter (Mapping Symbol *) FMin ((:->) Symbol * k v) xs), Sortable (Filter (Mapping Symbol *) FMax ((:->) Symbol * k v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((:) (Mapping Symbol *) ((:->) Symbol * k v) xs) | |
|
(Combinable v v', Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k (Combine * v v')) s)) => Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k v) ((:) (Mapping Symbol *) ((:->) Symbol * k v') s)) | |
|
Nubable ((:) (Mapping Symbol *) e ([] (Mapping Symbol *))) | |
|
((~) [Mapping Symbol *] (Nub Symbol * ((:) (Mapping Symbol *) e ((:) (Mapping Symbol *) f s))) ((:) (Mapping Symbol *) e (Nub Symbol * ((:) (Mapping Symbol *) f s))), Nubable ((:) (Mapping Symbol *) f s)) => Nubable ((:) (Mapping Symbol *) e ((:) (Mapping Symbol *) f s)) | |
|
Split s t st => Split ((:) (Mapping Symbol *) x s) t ((:) (Mapping Symbol *) x st) | |
|
Submap s t => Submap ((:) (Mapping Symbol *) x s) ((:) (Mapping Symbol *) x t) | |
|
Split s t st => Split ((:) (Mapping Symbol *) x s) ((:) (Mapping Symbol *) x t) ((:) (Mapping Symbol *) x st) | |
|
type Unit [Mapping Symbol *] IxCoreader Source # | |
|
type Unit [Mapping Symbol *] Reader Source # | |
|
type Unit [Mapping Symbol *] Writer Source # | |
|
type Meet [Mapping Symbol *] IxCoreader s t Source # | |
|
type CzipInv [Mapping Symbol *] IxCoreader s t Source # | |
|
type Inv [Mapping Symbol *] IxCoreader s t Source # | |
|
type Plus [Mapping Symbol *] IxCoreader s t Source # | |
|
type Plus [Mapping Symbol *] Reader f g Source # | |
|
type Plus [Mapping Symbol *] Writer s t Source # | |
|
type Inv [Mapping Symbol *] Reader f g Source # | |
|
type Inv [Mapping Symbol *] Writer s t Source # | |
|
type Cmp (Mapping Symbol v1) ((:->) Symbol v1 k v2) ((:->) Symbol v1 k' v') | |
|