diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/lux/abstract/equivalence.lux | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/stdlib/source/lux/abstract/equivalence.lux b/stdlib/source/lux/abstract/equivalence.lux index eacb4a48f..ccfc55928 100644 --- a/stdlib/source/lux/abstract/equivalence.lux +++ b/stdlib/source/lux/abstract/equivalence.lux @@ -8,13 +8,6 @@ (: (-> a a Bit) =)) -(def: #export (product left right) - (All [l r] (-> (Equivalence l) (Equivalence r) (Equivalence [l r]))) - (structure - (def: (= [a b] [x y]) - (and (:: left = a x) - (:: right = b y))))) - (def: #export (sum left right) (All [l r] (-> (Equivalence l) (Equivalence r) (Equivalence (| l r)))) (structure @@ -29,11 +22,18 @@ _ false)))) +(def: #export (product left right) + (All [l r] (-> (Equivalence l) (Equivalence r) (Equivalence [l r]))) + (structure + (def: (= [a b] [x y]) + (and (:: left = a x) + (:: right = b y))))) + (def: #export (rec sub) (All [a] (-> (-> (Equivalence a) (Equivalence a)) (Equivalence a))) (structure (def: (= left right) - (sub (rec sub) left right)))) + (sub = left right)))) (structure: #export contravariant (Contravariant Equivalence) |