| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Rerefined.Predicates.Operators
Contents
Description
Predicate re-exports using operators.
We stick with non-operators for base predicate definitions because, very simply, there aren't enough symbols to go around. The operators we would want to use for logical predicates are already being used on the term level, and I forsee a future full of promoted functions, so I wouldn't want to take up the type-level name.
Instead, I'm providing operators in separate modules. It's not ideal, because predicates already have operators defined in their pretty printing, and they may not coincide with available Haskell symbols. I'm not really sure how to do all this, it's very tentative for now.
Synopsis
- type (.&&) = And :: k -> k1 -> Type
- type (.||) = Or :: k -> k1 -> Type
- type (.<->) = Iff :: k -> k1 -> Type
- type (.->) = If :: k -> k1 -> Type
- type (.!&) = Nand :: k -> k1 -> Type
- type (.!|) = Nor :: k -> k1 -> Type
- type (.!) = Not :: k -> Type
- type (.!=) = Xor :: k -> k1 -> Type
- type (.<) = 'RelOpLT
- type (.<=) = 'RelOpLTE
- type (.==) = 'RelOpEQ
- type (./=) = 'RelOpNEQ
- type (.>=) = 'RelOpGTE
- type (.>) = 'RelOpGT
Logical
Awkward mix of Boolean and propositional operators. Sorry. Let me know if you have a better idea.