export fixity declarations

frex-project · Mar 30, 2024 · 8ba9723 · 8ba9723
1 parent 0bb1d1c
commit 8ba9723
Show file tree

Hide file tree

Showing 14 changed files with 17 additions and 17 deletions.
diff --git a/src/Data/Relation.idr b/src/Data/Relation.idr
@@ -6,7 +6,7 @@ public export
 0 Rel : Type -> Type
 Rel a = a -> a -> Type
 
-infix 5 ~>
+export infix 5 ~>
 public export
 0 (~>) : Rel a -> Rel a -> Type
 p ~> q = {x, y : a} -> p x y -> q x y
diff --git a/src/Data/Setoid/Definition.idr b/src/Data/Setoid/Definition.idr
@@ -7,7 +7,7 @@ import public Control.Order
 import Data.Vect
 import public Data.Fun.Nary
 
-infix 5 ~>, ~~>, <~>
+export infix 5 ~>, ~~>, <~>
 
 %default total
 

diff --git a/src/Frex/Algebra.idr b/src/Frex/Algebra.idr
@@ -27,8 +27,8 @@ import Data.Stream
 import Data.Name
 import Data.Vect.Extra
 
-infix 10 ^
-infix 5 ~>, <~>
+export infix 10 ^
+export infix 5 ~>, <~>
 
 %default total
 

diff --git a/src/Frex/Axiom.idr b/src/Frex/Axiom.idr
@@ -12,7 +12,7 @@ import Data.Fin
 
 %default total
 
-infix 1 =-=
+export infix 1 =-=
 
 ||| Smart constructor for making equations look nicer
 public export

diff --git a/src/Frex/Coproduct.idr b/src/Frex/Coproduct.idr
@@ -7,7 +7,7 @@ import Frex.Presentation
 import Frex.Algebra
 import Frex.Model
 
-infixr 3 <~.~>
+export infixr 3 <~.~>
 
 %default total
 

diff --git a/src/Frex/Free/Construction.idr b/src/Frex/Free/Construction.idr
@@ -16,7 +16,7 @@ import Text.PrettyPrint.Prettyprinter
 
 %default total
 
-infix 4 |-
+export infix 4 |-
 
 ||| Auxiliary abstraction: an algebra with a relation over it
 public export

diff --git a/src/Frex/Free/Construction/Linear.idr b/src/Frex/Free/Construction/Linear.idr
@@ -71,7 +71,7 @@ plug : (a : Algebra sig) ->
        (t : U a) -> U a
 plug a t u = bindTerm t (fromMaybe u)
 
-infixr 0 :.:
+export infixr 0 :.:
 public export
 (:.:) : {0 sig : Signature} ->
         Term sig (Maybe a) ->

diff --git a/src/Frex/Model.idr b/src/Frex/Model.idr
@@ -11,7 +11,7 @@ import Data.Vect.Extra
 import Data.Vect.Quantifiers
 import Data.Fin
 
-infix 1 =|
+export infix 1 =|
 
 %default total
 %ambiguity_depth 4

diff --git a/src/Notation/Additive.idr b/src/Notation/Additive.idr
@@ -7,7 +7,7 @@ import public Data.Fun.Extra
 
 %default total
 
-infixl 8 .+., :+:, |+|, +., +:, +|, .+, :+, |+
+export infixl 8 .+., :+:, |+|, +., +:, +|, .+, :+, |+
 
 public export
 interface Additive1 a where

diff --git a/src/Notation/Multiplicative.idr b/src/Notation/Multiplicative.idr
@@ -7,7 +7,7 @@ import public Data.Fun.Extra
 
 %default total
 
-infixl 9 .*., :*:, |*|, *., *:, *|, .*, :*, |*
+export infixl 9 .*., :*:, |*|, *., *:, *|, .*, :*, |*
 
 public export
 interface Multiplicative1 a where

diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
@@ -3,9 +3,9 @@ module Syntax.PreorderReasoning.Setoid
 
 import Data.Setoid.Definition
 
-infixl 0  ~~
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+export infixl 0  ~~
+export prefix 1  |~
+export infix  1  ...,..<,..>,.=.,.=<,.=>
 
 public export
 data Step : (a : Setoid) -> (lhs,rhs : U a) -> Type where

diff --git a/tests/frextests/certificates/Monoids.idr b/tests/frextests/certificates/Monoids.idr
@@ -18,7 +18,7 @@ import Syntax.PreorderReasoning
 
 import System.File
 
-infix 0 ~~
+export infix 0 ~~
 0 (~~) : Rel (U (Construction.Free MonoidTheory $ cast $ Fin n).Data.Model)
 (~~) = (Free MonoidTheory $ cast $ Fin n).Data.Model.rel
 

diff --git a/tests/frextests/printer/CommutativeMonoids.idr b/tests/frextests/printer/CommutativeMonoids.idr
@@ -33,7 +33,7 @@ Sta' = (FrexNat).Data.Embed.H.H
 Dyn' : {0 x : Type} -> x -> U (FrexNat {x}).Data.Model
 Dyn' = (FrexNat {x}).Data.Var.H
 
-infix 0 ~~
+export infix 0 ~~
 0 (~~) : (lhs, rhs : Term (EvaluationSig (CommutativeMonoidTheory).signature Nat) x) -> Type
 (~~) = (FrexNat).Data.Model.rel
 

diff --git a/tests/frextests/printer/Monoids.idr b/tests/frextests/printer/Monoids.idr
@@ -26,7 +26,7 @@ import System.File
   show _ = "boring"
 
 -- Using a concrete name so that the constraints when forming `X k` compute
-infix 0 ~~
+export infix 0 ~~
 (~~) : Term Signature (Fin 10) -> Term Signature (Fin 10) -> Type
 (~~) = (|-) {pres = MonoidTheory}
             (QuotientData MonoidTheory (irrelevantCast (Fin 10)))