export fixity declarations

ohad · Jul 26, 2024 · a35498d · a35498d
1 parent e496277
commit a35498d
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 7 deletions.
diff --git a/src/Collie.idr b/src/Collie.idr
@@ -55,7 +55,7 @@ public export
        Handlers a cmd
 (::) = MkHandlers
 
-infixr 4 ~~>
+export infixr 4 ~~>
 
 ||| A nicer notation for handlers
 public export

diff --git a/src/Collie/Modifiers.idr b/src/Collie/Modifiers.idr
@@ -8,7 +8,7 @@ import Data.Maybe
 
 %default total
 
-infix 4 ::=
+export infix 4 ::=
 public export
 (::=) : {0 a : String -> Type} -> (nm : String) -> a nm -> (nm : String ** a nm)
 (::=) = MkDPair

diff --git a/src/Data/List/Fresh.idr b/src/Data/List/Fresh.idr
@@ -17,7 +17,7 @@ public export
 BRel : Type -> Type
 BRel a = a -> a -> Bool
 
-infix 4 #, ##, #?
+export infix 4 #, ##, #?
 
 public export
 data FreshList : (a : Type) -> (neq : BRel a) -> Type

diff --git a/src/Data/List/Fresh/Quantifiers.idr b/src/Data/List/Fresh/Quantifiers.idr
@@ -52,7 +52,7 @@ removeFreshness (There pos) fresh =
   let (neq, fresh) = soAnd fresh in
   andSo (neq, removeFreshness pos fresh)
 
-infixr 4 !!
+export infixr 4 !!
 
 public export
 (!!) : (prfs : All p xs) -> (pos : Any q xs) -> p (lookup pos)

diff --git a/src/Data/Magma.idr b/src/Data/Magma.idr
@@ -4,7 +4,7 @@ import Data.Maybe
 
 %default total
 
-infixr 6 .*.
+export infixr 6 .*.
 
 public export
 record RawMagma where

diff --git a/src/Data/Record/SmartConstructors.idr b/src/Data/Record/SmartConstructors.idr
@@ -9,6 +9,7 @@ import Data.Record
 
 %default total
 
+export infix 1 ::=
 namespace Check
 
   public export
@@ -19,7 +20,6 @@ namespace Check
     constructor MkCheckable
     mkCheckable : Record f flds
 
-  infix 1 ::=
   public export
   record Entry
     (a    : String -> Type)
@@ -55,7 +55,6 @@ namespace Infer
     constructor MkInferrable
     mkInferrable : Record f flds
 
-  infix 1 ::=
   public export
   record Entry (a : String -> Type) (f : Field a -> Type) where
     constructor (::=)