Merge pull request #20 from stefan-hoeck/export_infix

[ compat ] add export modifier to operator decls
stefan-hoeck · Apr 5, 2024 · 829f44b · 829f44b
2 parents f60b0da + 6c5c59e
commit 829f44b
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/Algebra/Group.idr b/src/Algebra/Group.idr
@@ -12,9 +12,9 @@ import Syntax.PreorderReasoning
 --          "Operators"
 --------------------------------------------------------------------------------
 
-infixl 8 `p`,`sub`
+export infixl 8 `p`,`sub`
 
-infixl 9 `m`
+export infixl 9 `m`
 
 --------------------------------------------------------------------------------
 --          Laws

diff --git a/src/Algebra/Solver/Ops.idr b/src/Algebra/Solver/Ops.idr
@@ -2,7 +2,7 @@ module Algebra.Solver.Ops
 
 import public Data.List.Elem
 
-infixl 8 .+>, <+., .+.
+export infixl 8 .+>, <+., .+.
 
 ||| Checks if elements `x` and `y` are at the same position in list
 ||| `xs` and thus identical.

diff --git a/src/Algebra/Solver/Semiring.idr b/src/Algebra/Solver/Semiring.idr
@@ -82,9 +82,9 @@ public export
 var : {0 as : List a} -> (x : a) -> Elem x as => Expr a as
 var x = Var x %search
 
-infixl 8 .+., .+, +.
+export infixl 8 .+., .+, +.
 
-infixl 9 .*., .*, *.
+export infixl 9 .*., .*, *.
 
 ||| Addition of variables. This is an alias for
 ||| `var x + var y`.