| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Rerefined.Simplify.Relational
Description
Relational predicate simplification.
These bits aren't mutually recursive with the main simplifier, so we can keep them separate for a bit of code hygiene.
Internal module. Exports may change without warning. Try not to use.
Documentation
type family SimplifyCompareLength (op :: RelOp) (n :: Natural) :: Maybe Type where ... Source #
Equations
| SimplifyCompareLength 'RelOpLT 0 = 'Just Fail | |
| SimplifyCompareLength 'RelOpLTE 0 = 'Just (CompareLength 'RelOpEQ 0) | |
| SimplifyCompareLength 'RelOpGTE 0 = 'Just Succeed | |
| SimplifyCompareLength 'RelOpGT 0 = 'Just (CompareLength 'RelOpEQ 0) | |
| SimplifyCompareLength op n = 'Nothing :: Maybe Type |
type family SimplifyCompareLengthAnd (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) :: Maybe Type where ... Source #
Equations
| SimplifyCompareLengthAnd 'RelOpLT n 'RelOpGT m = OrdCond (CmpNat n m) ('Just Fail) ('Just Fail) ('Nothing :: Maybe Type) | |
| SimplifyCompareLengthAnd 'RelOpGT m 'RelOpLT n = OrdCond (CmpNat n m) ('Just Fail) ('Just Fail) ('Nothing :: Maybe Type) | |
| SimplifyCompareLengthAnd lop ln rop rn = 'Nothing :: Maybe Type |
type family SimplifyCompareLengthOr (lop :: RelOp) (ln :: Natural) (rop :: RelOp) (rn :: Natural) :: Maybe Type where ... Source #
Equations
| SimplifyCompareLengthOr 'RelOpLT n 'RelOpGT m = OrdCond (CmpNat n m) ('Nothing :: Maybe Type) ('Just (CompareLength 'RelOpNEQ n)) ('Just Succeed) | |
| SimplifyCompareLengthOr 'RelOpGT m 'RelOpLT n = OrdCond (CmpNat n m) ('Nothing :: Maybe Type) ('Just (CompareLength 'RelOpNEQ n)) ('Just Succeed) | |
| SimplifyCompareLengthOr lop ln rop rn = 'Nothing :: Maybe Type |