lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Constraint.hs (607B)

      1 --------------------------------------------------------------------------------
      2 
      3 -- type AllSatisfy :: forall {i}. Predicate i -> List i -> Constraint
      4 -- type family AllSatisfy p xs where
      5 --     AllSatisfy _ [] = Verum
      6 --     AllSatisfy p (x : xs) = p x :& AllSatisfy p xs
      7 
      8 -- type BothSatisfy :: forall {i}. Predicate i -> i -> i -> Constraint
      9 -- class (p x, p y) => BothSatisfy p x y
     10 -- instance (p x, p y) => BothSatisfy p x y
     11 -- instance forall a p x y. (a `Witnesses` p x, a `Witnesses` p y) => a `Witnesses` BothSatisfy p x y where
     12 --     witness _ a = Evidence \\ witness (p x) a \\ witness (p y) a