diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:55:09 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:55:09 +0000 |
| commit | 332f481a61429c031016fd5d43238095d1a22075 (patch) | |
| tree | 7946554f7bbfe498674b2f5e7fcf456c8162fb0c /src/Soat/FirstOrder/Algebra/Coproduct.idr | |
| parent | 1f378ce7d61e16a3dc805ce63f87b5b8202f3f8e (diff) | |
refactor : rename homomorphism combinators.
- idHomo -> id
- compHomo -> (.)
Diffstat (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index a98391b..5cb4c45 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -195,8 +195,8 @@ coproductUnique' : {x, y, z : Algebra sig} -> z.relation t (f.func t tm) (g.func t tm) coproductUnique' f g congL congR tm = bindUnique' { v = fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i)) - , f = compHomo f $ termToCoproduct x y - , g = compHomo g $ termToCoproduct x y + , f = f . termToCoproduct x y + , g = g . termToCoproduct x y , cong = \x => case x of (Left x) => congL x (Right x) => congR x |