From fcd024cb01e484dc3c92212f4317b254bbd7580b Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 6 Dec 2022 16:18:29 +0000 Subject: Add smart constructor for first-order algebras. --- src/Soat/FirstOrder/Algebra/Coproduct.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Soat/FirstOrder/Algebra/Coproduct.idr') diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index 548beed..041d650 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -93,7 +93,7 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra public export CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig -CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra +CoproductAlgebra x y = MakeAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra public export injectLHomo : x ~> CoproductAlgebra x y -- cgit v1.2.3