|
|
|
|
|
Description |
- Sets are encoded as certain types of kind * -> *
- A value of type S X is a proof that the type X is a member of S
|
|
Synopsis |
|
|
|
|
Subsets, equality
|
|
|
|
data set1 :⊆: set2 where | Source |
|
Represents a proof that set1 is a subset of set2
| Constructors | Subset :: (forall a. (a :∈: set1) -> a :∈: set2) -> set1 :⊆: set2 | |
| Instances | |
|
|
|
Coercion from subset to superset
|
|
|
|
|
Extensional equality of sets
| Constructors | SetEq (set1 :⊆: set2) (set2 :⊆: set1) | |
| Instances | |
|
|
|
Coercion using a set equality
|
|
|
Coercion using a set equality (flipped)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Union, intersection, difference
|
|
|
Binary union
| Constructors | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Binary intersection
| Constructors | Inter :: (a :∈: s1) -> (a :∈: s2) -> (s1 :∩: s2) a | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Union of a family
| Constructors | |
|
|
|
|
|
Dependent sum
| Constructors | |
|
|
|
|
|
Intersection of a family
| Constructors | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Set difference
| Constructors | |
|
|
|
|
Products
|
|
|
Binary products
| Constructors | :×: :: (a :∈: s1) -> (b :∈: s2) -> (s1 :×: s2) (a, b) | |
|
|
|
|
|
|
|
|
|
|
Product is monotonic wrt. subset inclusion
|
|
Particular sets
|
|
|
Empty set (barring cheating with undefined)
| Constructors | Empty :: (forall b. b) -> Empty a | |
|
|
|
|
|
|
|
|
Set of all types of kind *
| Constructors | |
|
|
|
|
|
Constructors | | Instances | |
|
|
|
|
data KleisliType m where | Source |
|
Constructors | | Instances | |
|
|
|
|
data CoKleisliType w where | Source |
|
Constructors | | Instances | |
|
|
|
|
Sets from common typeclasses
|
|
|
Constructors | | Instances | |
|
|
|
Example application
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
|
|
Constructors | | Instances | |
|
|
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
data FractionalType where | Source |
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
Kind (* -> *)
|
|
|
Constructors | | Instances | |
|
|
|
|
|
Constructors | | Instances | |
|
|
data MonadPlusType where | Source |
|
Constructors | | Instances | |
|
|
data ApplicativeType where | Source |
|
Constructors | | Instances | |
|
|
Powerset
|
|
|
Membership of a set in a set representing a set of sets
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Misc
|
|
|
|
|
|
|
|
|
Unique existence of sets
|
|
|
Unique existence, unlowered
| Constructors | ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p | |
|
|
|
From sets to the value level
|
|
|
V s is the sum of all types x such that s x is provable.
| Constructors | | Instances | |
|
|
|
|
|
|
|
|
Produced by Haddock version 2.4.2 |