diff --git a/src/Collie.idr b/src/Collie.idr
index 2e989d7..2b128c7 100644
--- 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
index e44db80..cd22192 100644
--- 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
index 06814bc..f19b5c0 100644
--- 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
index f6bfd25..efbbb47 100644
--- 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
index 2f29ec4..4c7c044 100644
--- 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
index 17e32b0..9d6ab3c 100644
--- 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 (::=)