Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data Constraint z r c where
- (:==) :: Linear z r c k1 -> Linear z r c k2 -> Constraint z r c
- (:<=) :: Linear z r c k1 -> Linear z r c k2 -> Constraint z r c
- (:<) :: Linear z r c KZ -> Linear z r c KZ -> Constraint z r c
- (:>=) :: Linear z r c k1 -> Linear z r c k2 -> Constraint z r c
- (:>) :: Linear z r c KZ -> Linear z r c KZ -> Constraint z r c
- Between :: Linear z r c k1 -> Linear z r c k2 -> Linear z r c k3 -> Constraint z r c
- (:&&) :: Constraint z r c -> Constraint z r c -> Constraint z r c
- (:!) :: String -> Constraint z r c -> Constraint z r c
- CTrue :: Constraint z r c
Documentation
data Constraint z r c where Source #
Different kind of constraints.
These are not all necessary, but I have a hunch that keeping some structure may be helpful in the future.
Constructors:
:==
- Equality constraint
:<=
- Less than or equal
:<
- Strictly less than: this is only allowed for purely integer functions
:>=
- Greater than or equal
:>
- Strictly greater than: this is only allowed for purely integer functions
Between
Between a b c
is equivalent toa :<= b :&& b :<= c
:&&
- Conjunction of two constraints
:!
"name" :! constr
Annotate a constraint with a name, or other useless informationCTrue
- Trivially true constraint
(:==) :: Linear z r c k1 -> Linear z r c k2 -> Constraint z r c infix 5 | |
(:<=) :: Linear z r c k1 -> Linear z r c k2 -> Constraint z r c infix 5 | |
(:<) :: Linear z r c KZ -> Linear z r c KZ -> Constraint z r c infix 5 | |
(:>=) :: Linear z r c k1 -> Linear z r c k2 -> Constraint z r c infix 5 | |
(:>) :: Linear z r c KZ -> Linear z r c KZ -> Constraint z r c infix 5 | |
Between :: Linear z r c k1 -> Linear z r c k2 -> Linear z r c k3 -> Constraint z r c | |
(:&&) :: Constraint z r c -> Constraint z r c -> Constraint z r c infixr 3 | |
(:!) :: String -> Constraint z r c -> Constraint z r c infix 4 | |
CTrue :: Constraint z r c |