lude

commit 49a01b92e7a020244dd2b1de820b5d16a5404661
parent 7e981456d81795e178028c11d94d324d99b0bdec
Author: Robert Russell <robert@rr3.xyz>
Date:   Mon, 21 Sep 2026 16:21:09 -0700

Add/remove some TODOs

Diffstat:
M
TODO.md
 | 
2
++
D
Todo/Constraint.hs
 | 
12
------------
M
src/Lude/Constraint/Predicate.hs
 | 
8
++++++++

3 files changed, 10 insertions(+), 12 deletions(-)
diff --git a/TODO.md b/TODO.md
@@ -5,3 +5,5 @@
 - Put Flt{32,64} as a TODO.
 - Text/String
 - containers
+- Some, All, End, Coend, etc.
+- Reduce hom functor dupe with defaults exported from Hom
diff --git a/Todo/Constraint.hs b/Todo/Constraint.hs
@@ -1,12 +0,0 @@
---------------------------------------------------------------------------------
-
--- type AllSatisfy :: forall {i}. Predicate i -> List i -> Constraint
--- type family AllSatisfy p xs where
---     AllSatisfy _ [] = Verum
---     AllSatisfy p (x : xs) = p x :& AllSatisfy p xs
-
--- type BothSatisfy :: forall {i}. Predicate i -> i -> i -> Constraint
--- class (p x, p y) => BothSatisfy p x y
--- instance (p x, p y) => BothSatisfy p x y
--- instance forall a p x y. (a `Witnesses` p x, a `Witnesses` p y) => a `Witnesses` BothSatisfy p x y where
---     witness _ a = Evidence \\ witness (p x) a \\ witness (p y) a
diff --git a/src/Lude/Constraint/Predicate.hs b/src/Lude/Constraint/Predicate.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE IncoherentInstances #-}
 
 module Lude.Constraint.Predicate (
+    -- AllSatisfy,
     Always,
     always,
     Never,
@@ -16,6 +17,13 @@ import Lude.Haskell
 
 --------------------------------------------------------------------------------
 
+-- type AllSatisfy :: forall {i}. Predicate i -> List i -> Constraint
+-- type family AllSatisfy p xs where
+--     AllSatisfy _ [] = Verum
+--     AllSatisfy p (x : xs) = p x & AllSatisfy p xs
+
+--------------------------------------------------------------------------------
+
 type role Always phantom
 type Always :: forall {i}. Predicate i
 class Always x