diff --git a/libs/base/Data/Bits.idr b/libs/base/Data/Bits.idr
index 68bc156cbd..0d3ce45e1a 100644
--- a/libs/base/Data/Bits.idr
+++ b/libs/base/Data/Bits.idr
@@ -5,10 +5,10 @@ import Data.Vect
 
 %default total
 
-infixl 8 `shiftL`, `shiftR`
-infixl 7 .&.
-infixl 6 `xor`
-infixl 5 .|.
+export infixl 8 `shiftL`, `shiftR`
+export infixl 7 .&.
+export infixl 6 `xor`
+export infixl 5 .|.
 
 --------------------------------------------------------------------------------
 --          Interface Bits
diff --git a/libs/base/Data/Contravariant.idr b/libs/base/Data/Contravariant.idr
index b0d441b6e4..098d66a42a 100644
--- a/libs/base/Data/Contravariant.idr
+++ b/libs/base/Data/Contravariant.idr
@@ -2,7 +2,7 @@ module Data.Contravariant
 
 %default total
 
-infixl 4 >$, >$<, >&<, $<
+export infixl 4 >$, >$<, >&<, $<
 
 ||| Contravariant functors
 public export
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index edc1d16daa..e879de24e4 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -270,7 +270,7 @@ public export
 deleteFirstsBy : (p : a -> b -> Bool) -> (source : List b) -> (undesirables : List a) -> List b
 deleteFirstsBy p = foldl (flip (deleteBy p))
 
-infix 7 \\
+export infix 7 \\
 
 ||| The non-associative list-difference.
 ||| A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@
diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr
index 1b02fb5cbc..072ad92681 100644
--- a/libs/base/Data/List1.idr
+++ b/libs/base/Data/List1.idr
@@ -5,7 +5,7 @@ import public Control.Function
 
 %default total
 
-infixr 7 :::
+export infixr 7 :::
 
 ||| Non-empty lists.
 public export
diff --git a/libs/base/Data/Morphisms.idr b/libs/base/Data/Morphisms.idr
index d25c2c0108..9b0cb356b9 100644
--- a/libs/base/Data/Morphisms.idr
+++ b/libs/base/Data/Morphisms.idr
@@ -9,7 +9,7 @@ record Morphism a b where
   constructor Mor
   applyMor : a -> b
 
-infixr 1 ~>
+export infixr 1 ~>
 
 public export
 (~>) : Type -> Type -> Type
diff --git a/libs/base/Data/Zippable.idr b/libs/base/Data/Zippable.idr
index c4ee8f47e2..75c72114a4 100644
--- a/libs/base/Data/Zippable.idr
+++ b/libs/base/Data/Zippable.idr
@@ -21,7 +21,7 @@ interface Zippable z where
   zip : z a -> z b -> z (a, b)
   zip = zipWith (,)
 
-  infixr 6 `zip`
+  export infixr 6 `zip`
 
   ||| Combine three parameterised types by applying a function.
   ||| @ z the parameterised type
diff --git a/libs/base/Syntax/PreorderReasoning.idr b/libs/base/Syntax/PreorderReasoning.idr
index e5ab959980..82e429fdac 100644
--- a/libs/base/Syntax/PreorderReasoning.idr
+++ b/libs/base/Syntax/PreorderReasoning.idr
@@ -2,9 +2,7 @@
 ||| poor-man's equational reasoning
 module Syntax.PreorderReasoning
 
-infixl 0  ~~,~=
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+import public Syntax.PreorderReasoning.Ops
 
 |||Slightly nicer syntax for justifying equations:
 |||```
diff --git a/libs/base/Syntax/PreorderReasoning/Generic.idr b/libs/base/Syntax/PreorderReasoning/Generic.idr
index b52f71ba4e..2f77322698 100644
--- a/libs/base/Syntax/PreorderReasoning/Generic.idr
+++ b/libs/base/Syntax/PreorderReasoning/Generic.idr
@@ -2,10 +2,7 @@ module Syntax.PreorderReasoning.Generic
 
 import Control.Relation
 import Control.Order
-infixl 0  ~~, ~=
-infixl 0  <~
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+import public Syntax.PreorderReasoning.Ops
 
 public export
 data Step : (leq : a -> a -> Type) -> a -> a -> Type where
diff --git a/libs/base/Syntax/PreorderReasoning/Ops.idr b/libs/base/Syntax/PreorderReasoning/Ops.idr
new file mode 100644
index 0000000000..ae3cc8ea92
--- /dev/null
+++ b/libs/base/Syntax/PreorderReasoning/Ops.idr
@@ -0,0 +1,6 @@
+module Syntax.PreorderReasoning.Ops
+
+export infixl 0  ~~, ~=
+export infixl 0  <~
+export prefix 1  |~
+export infix  1  ...,..<,..>,.=.,.=<,.=>
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 0250fe775c..0b4a920a48 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -108,6 +108,7 @@ modules = Control.App,
           Language.Reflection.TTImp,
 
           Syntax.PreorderReasoning,
+          Syntax.PreorderReasoning.Ops,
           Syntax.PreorderReasoning.Generic,
 
           System,
diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
index f8d877ffa5..6fa1fc9eb8 100644
--- a/libs/contrib/Control/Algebra.idr
+++ b/libs/contrib/Control/Algebra.idr
@@ -1,7 +1,7 @@
 module Control.Algebra
 
-infixl 6 <->
-infixl 7 <.>
+export infixl 6 <->
+export infixl 7 <.>
 
 public export
 interface Semigroup ty => SemigroupV ty where
diff --git a/libs/contrib/Control/Arrow.idr b/libs/contrib/Control/Arrow.idr
index 13922d3b60..26fe8f12cb 100644
--- a/libs/contrib/Control/Arrow.idr
+++ b/libs/contrib/Control/Arrow.idr
@@ -5,11 +5,11 @@ import Data.Either
 import Data.Morphisms
 
 
-infixr 5 <++>
-infixr 3 ***
-infixr 3 &&&
-infixr 2 +++
-infixr 2 \|/
+export infixr 5 <++>
+export infixr 3 ***
+export infixr 3 &&&
+export infixr 2 +++
+export infixr 2 \|/
 
 public export
 interface Category arr => Arrow (0 arr : Type -> Type -> Type) where
diff --git a/libs/contrib/Control/Category.idr b/libs/contrib/Control/Category.idr
index 1c0e72bb87..bf59a96d0d 100644
--- a/libs/contrib/Control/Category.idr
+++ b/libs/contrib/Control/Category.idr
@@ -20,7 +20,7 @@ Monad m => Category (Kleislimorphism m) where
   id                        = Kleisli (pure . id)
   (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
 
-infixr 1 >>>
+export infixr 1 >>>
 
 public export
 (>>>) : Category cat => cat a b -> cat b c -> cat a c
diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
index 00317c7879..3357f9affd 100644
--- a/libs/contrib/Control/Validation.idr
+++ b/libs/contrib/Control/Validation.idr
@@ -96,7 +96,7 @@ export
 fail : Applicative m => String -> ValidatorT m a b
 fail s = MkValidator $ \_ => left s
 
-infixl 2 >>>
+export infixl 2 >>>
 
 ||| Compose two validators so that the second validates the output of the first.
 export
diff --git a/libs/contrib/Data/List/Alternating.idr b/libs/contrib/Data/List/Alternating.idr
index b80d19aaae..eb62d1ed22 100644
--- a/libs/contrib/Data/List/Alternating.idr
+++ b/libs/contrib/Data/List/Alternating.idr
@@ -3,8 +3,8 @@ module Data.List.Alternating
 import Data.Bifoldable
 import Data.List
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 %default total
 
diff --git a/libs/contrib/Data/Monoid/Exponentiation.idr b/libs/contrib/Data/Monoid/Exponentiation.idr
index d2e44bbb3a..f7ddbe386f 100644
--- a/libs/contrib/Data/Monoid/Exponentiation.idr
+++ b/libs/contrib/Data/Monoid/Exponentiation.idr
@@ -23,7 +23,7 @@ public export
 modular : Monoid a => a -> Nat -> a
 modular v n = modularRec v (halfRec n)
 
-infixr 10 ^
+export infixr 10 ^
 public export
 (^) : Num a => a -> Nat -> a
 (^) = modular @{Multiplicative}
diff --git a/libs/contrib/Data/Seq/Internal.idr b/libs/contrib/Data/Seq/Internal.idr
index b9cf10664f..a54f39c4ac 100644
--- a/libs/contrib/Data/Seq/Internal.idr
+++ b/libs/contrib/Data/Seq/Internal.idr
@@ -342,7 +342,7 @@ viewRTree (Deep s pr m (Four w x y z)) =
 
 
 -- Construction
-infixr 5 `consTree`
+export infixr 5 `consTree`
 export
 consTree : Sized e => (r : e) -> FingerTree e -> FingerTree e
 a `consTree` Empty                       = Single a
@@ -352,7 +352,7 @@ a `consTree` Deep s (Two b c) st d2      = Deep (size a + s) (Three a b c) st d2
 a `consTree` Deep s (Three b c d) st d2  = Deep (size a + s) (Four a b c d) st d2
 a `consTree` Deep s (Four b c d f) st d2 = Deep (size a + s) (Two a b) (node3 c d f `consTree` st) d2
 
-infixl 5 `snocTree`
+export infixl 5 `snocTree`
 export
 snocTree : Sized e => FingerTree e -> (r : e) -> FingerTree e
 Empty `snocTree` a                       = Single a
diff --git a/libs/contrib/Data/Seq/Sized.idr b/libs/contrib/Data/Seq/Sized.idr
index 43578cbd76..79ca527cc1 100644
--- a/libs/contrib/Data/Seq/Sized.idr
+++ b/libs/contrib/Data/Seq/Sized.idr
@@ -48,13 +48,13 @@ export
 reverse : Seq n a -> Seq n a
 reverse (MkSeq tr) = MkSeq (reverseTree id tr)
 
-infixr 5 `cons`
+export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
 export
 cons : e -> Seq n e -> Seq (S n) e
 a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
 
-infixl 5 `snoc`
+export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
 export
 snoc : Seq n e -> e -> Seq (S n) e
diff --git a/libs/contrib/Data/Seq/Unsized.idr b/libs/contrib/Data/Seq/Unsized.idr
index cb0eb28f53..ce011cc97c 100644
--- a/libs/contrib/Data/Seq/Unsized.idr
+++ b/libs/contrib/Data/Seq/Unsized.idr
@@ -40,13 +40,13 @@ export
 reverse : Seq a -> Seq a
 reverse (MkSeq tr) = MkSeq (reverseTree id tr)
 
-infixr 5 `cons`
+export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
 export
 cons : e -> Seq e -> Seq e
 a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
 
-infixl 5 `snoc`
+export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
 export
 snoc : Seq e -> e -> Seq e
diff --git a/libs/contrib/Data/String/Extra.idr b/libs/contrib/Data/String/Extra.idr
index 40f45b84af..418bd47462 100644
--- a/libs/contrib/Data/String/Extra.idr
+++ b/libs/contrib/Data/String/Extra.idr
@@ -5,8 +5,8 @@ import Data.String
 
 %default total
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 ||| Adds a character to the end of the specified string.
 |||
diff --git a/libs/contrib/Data/String/Parser.idr b/libs/contrib/Data/String/Parser.idr
index 4de6f12f4c..bf5b46121d 100644
--- a/libs/contrib/Data/String/Parser.idr
+++ b/libs/contrib/Data/String/Parser.idr
@@ -106,7 +106,7 @@ export
                                 Fail i _ => Fail i msg)
                             (p.runParser s)
 
-infixl 0 <?>
+export infixl 0 <?>
 
 ||| Discards the result of a parser
 export
diff --git a/libs/contrib/Data/Telescope/Segment.idr b/libs/contrib/Data/Telescope/Segment.idr
index 88c0773204..1d97e6a95f 100644
--- a/libs/contrib/Data/Telescope/Segment.idr
+++ b/libs/contrib/Data/Telescope/Segment.idr
@@ -59,7 +59,7 @@ toTelescope seg = untabulate seg ()
 
 %name Segment delta,delta',delta1,delta2
 
-infixl 3 |++, :++
+export infixl 3 |++, :++
 
 ||| This lemma comes up all the time when mixing induction on Nat with
 ||| indexing modulo addition.  An alternative is to use something like
@@ -141,7 +141,7 @@ projection {n = S n} {delta = ty :: delta} env
                     $ rewrite succLemma n k in env
     in env'
 
-infixl 4 .=
+export infixl 4 .=
 
 public export
 data Environment : (env : Left.Environment gamma)
diff --git a/libs/contrib/Data/Telescope/Telescope.idr b/libs/contrib/Data/Telescope/Telescope.idr
index d46f308e7e..d4dbdc4195 100644
--- a/libs/contrib/Data/Telescope/Telescope.idr
+++ b/libs/contrib/Data/Telescope/Telescope.idr
@@ -30,8 +30,8 @@ plusAccZeroRightNeutral m =
   Refl
 
 
-infixl 4 -.
-infixr 4 .-
+export infixl 4 -.
+export infixr 4 .-
 
 namespace Left
 
@@ -158,7 +158,7 @@ namespace Right
 
 namespace Tree
 
-  infixl 4 ><
+  export infixl 4 ><
 
   mutual
     ||| A tree of dependent types
@@ -189,14 +189,14 @@ namespace Tree
          (transpL env1 ** snd (concat (delta (transpL env1))) env2)
     )
 
-infix 5 <++>
+export infix 5 <++>
 
 public export
 (<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
 [] <++> delta = delta ()
 (gamma -. sigma ) <++> delta = gamma <++> (\ env => sigma env .- \ v => delta (env ** v))
 
-infix 5 >++<
+export infix 5 >++<
 
 (>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
          Left.Telescope (plusAcc m n)
diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr
index 1b43bd56e4..603f6f9bbd 100644
--- a/libs/contrib/System/Path.idr
+++ b/libs/contrib/System/Path.idr
@@ -13,8 +13,8 @@ import Text.Quantity
 
 import System.Info
 
-infixl 5 </>, />
-infixr 7 <.>
+export infixl 5 </>, />
+export infixr 7 <.>
 
 
 ||| The character that separates directories in the path.
diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr
index 93db72bb9a..2dc7c9812f 100644
--- a/libs/contrib/Text/Parser/Core.idr
+++ b/libs/contrib/Text/Parser/Core.idr
@@ -128,7 +128,7 @@ export %inline
         Grammar state tok (c1 && c2) ty
 (<|>) = Alt
 
-infixr 2 <||>
+export infixr 2 <||>
 ||| Take the tagged disjunction of two grammars. If both consume, the
 ||| combination is guaranteed to consume.
 export
diff --git a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr b/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr
index 97fb9f7d30..c2ec32d498 100644
--- a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr
+++ b/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr
@@ -122,7 +122,7 @@ export
 fill : Int -> Doc ann -> Doc ann
 fill n doc = width doc (\w => spaces $ n - w)
 
-infixr 6 <++>
+export infixr 6 <++>
 ||| Concatenates two documents with a space in between.
 export
 (<++>) : Doc ann -> Doc ann -> Doc ann
diff --git a/libs/linear/Data/Linear/Interface.idr b/libs/linear/Data/Linear/Interface.idr
index ec7d857aeb..6a8f5fcfe2 100644
--- a/libs/linear/Data/Linear/Interface.idr
+++ b/libs/linear/Data/Linear/Interface.idr
@@ -35,7 +35,7 @@ Consumable Int where
 
 -- But crucially we don't have `Consumable World` or `Consumable Handle`.
 
-infixr 5 `seq`
+export infixr 5 `seq`
 ||| We can sequentially compose a computation returning a value that is
 ||| consumable with another computation. This is done by first consuming
 ||| the result of the first computation and then returning the second one.
diff --git a/libs/linear/Data/Linear/Notation.idr b/libs/linear/Data/Linear/Notation.idr
index 11989ec35c..35ce2d5b88 100644
--- a/libs/linear/Data/Linear/Notation.idr
+++ b/libs/linear/Data/Linear/Notation.idr
@@ -2,7 +2,7 @@ module Data.Linear.Notation
 
 %default total
 
-infixr 0 -@
+export infixr 0 -@
 ||| Infix notation for linear implication
 public export
 (-@) : Type -> Type -> Type
diff --git a/libs/papers/Data/Description/Regular.idr b/libs/papers/Data/Description/Regular.idr
index c4a0251f6e..0b904c35b8 100644
--- a/libs/papers/Data/Description/Regular.idr
+++ b/libs/papers/Data/Description/Regular.idr
@@ -88,7 +88,7 @@ Memo (Const s prop) x b = (v : s) -> b v
 Memo (d1 * d2) x b = Memo d1 x $ \ v1 => Memo d2 x $ \ v2 => b (v1, v2)
 Memo (d1 + d2) x b = (Memo d1 x (b . Left), Memo d2 x (b . Right))
 
-infixr 0 ~>
+export infixr 0 ~>
 
 ||| A memo trie is a coinductive structure
 export
diff --git a/libs/papers/Data/W.idr b/libs/papers/Data/W.idr
index b8dcd4f7a6..e92e46ab55 100644
--- a/libs/papers/Data/W.idr
+++ b/libs/papers/Data/W.idr
@@ -66,12 +66,12 @@ namespace Finitary
   Arr (AUnit nm) r = One nm r
   Arr (d || e) r = (Arr d r, Arr e r)
 
-  infixr 0 ~>
+  export infixr 0 ~>
   record (~>) (d : Fin) (r : Type) where
     constructor MkArr
     runArr : Arr d r
 
-  infix 5 .=
+  export infix 5 .=
   (.=) : (nm : String) -> s -> One nm s
   nm .= v = MkOne v
 
@@ -98,7 +98,7 @@ namespace Finitary
   appArr (d || e) f (Left x) = appArr d (fst f) x
   appArr (d || e) f (Right x) = appArr e (snd f) x
 
-  infixl 0 $$
+  export infixl 0 $$
   ($$) : {d : Fin} -> (d ~> r) -> (Elem d -> r)
   MkArr f $$ x = appArr d f x
 
diff --git a/libs/papers/Language/IntrinsicScoping/TypeTheory.idr b/libs/papers/Language/IntrinsicScoping/TypeTheory.idr
index c64aa33f53..9539e6c74f 100644
--- a/libs/papers/Language/IntrinsicScoping/TypeTheory.idr
+++ b/libs/papers/Language/IntrinsicScoping/TypeTheory.idr
@@ -76,7 +76,7 @@ data Infer : Scoped where
   ||| The application of a function to its argument
   App : Infer f g -> Check f g -> Infer f g
 
-infixl 3 `App`
+export infixl 3 `App`
 
 %name Infer e
 
@@ -229,7 +229,7 @@ namespace Value
 vfree : Level nm f -> Value f
 vfree x = VEmb (NVar x)
 
-infixl 5 `vapp`
+export infixl 5 `vapp`
 
 ||| We can easily apply a value standing for a function
 ||| to a value standing for its argument by either deploying
diff --git a/libs/papers/Language/Tagless.idr b/libs/papers/Language/Tagless.idr
index 1e90bd6298..1378cbf34a 100644
--- a/libs/papers/Language/Tagless.idr
+++ b/libs/papers/Language/Tagless.idr
@@ -9,7 +9,7 @@ import Data.List.Quantifiers
 
 %default total
 
-infixr 0 -#
+export infixr 0 -#
 public export
 (-#) : Type -> Type -> Type
 a -# b = (0 _ : a) -> b
diff --git a/libs/papers/Language/TypeTheory.idr b/libs/papers/Language/TypeTheory.idr
index 2065a90669..6845ca4d35 100644
--- a/libs/papers/Language/TypeTheory.idr
+++ b/libs/papers/Language/TypeTheory.idr
@@ -15,6 +15,8 @@ import Data.List
 
 %default covering
 
+private infixl 3 `App`
+
 ||| We use this wrapper to mark places where binding occurs.
 ||| This is a major footgun and we hope the type constructor
 ||| forces users to think carefully about what they are doing
@@ -55,7 +57,7 @@ namespace Section2
     Quote m == Quote n = m == n
     _ == _ = False
 
-  infixr 0 ~>
+  private infixr 0 ~>
   total
   data Ty : Type where
     ||| A family of base types
@@ -91,8 +93,6 @@ namespace Section2
     ||| The application of a function to its argument
     App : Infer -> Check -> Infer
 
-  infixl 3 `App`
-
   %name Infer e, f
 
   total
@@ -359,7 +359,6 @@ namespace Section3
     ||| The application of a function to its argument
     App : Infer -> Check -> Infer
 
-  infixl 3 `App`
 
   %name Infer e, f
 
@@ -600,8 +599,6 @@ namespace Section4
     ||| The application of a function to its argument
     App : Infer -> Check -> Infer
 
-  infixl 3 `App`
-
   %name Infer e, f
 
   total
@@ -695,7 +692,7 @@ namespace Section4
   vfree : Name -> Value
   vfree x = VEmb (NVar x)
 
-  infixl 5 `vapp`
+  private infixl 5 `vapp`
 
   ||| We can easily apply a value standing for a function
   ||| to a value standing for its argument by either deploying
diff --git a/libs/papers/Search/HDecidable.idr b/libs/papers/Search/HDecidable.idr
index 32c2298cb7..6089165271 100644
--- a/libs/papers/Search/HDecidable.idr
+++ b/libs/papers/Search/HDecidable.idr
@@ -114,7 +114,7 @@ not : (AnHDec l, Negates na a) => l na -> HDec (Not a)
 not p = [| toNegation (toHDec p) |]
 
 
-infixr 3 ==>
+export infixr 3 ==>
 
 ||| Half deciders are closed under implication
 public export
diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr
index 1a839238d7..85e778142f 100644
--- a/libs/prelude/Builtin.idr
+++ b/libs/prelude/Builtin.idr
@@ -74,7 +74,7 @@ swap (x, y) = (y, x)
 -- This directive tells auto implicit search what to use to look inside pairs
 %pair Pair fst snd
 
-infixr 5 #
+export infixr 5 #
 
 ||| A pair type where each component is linear
 public export
@@ -126,7 +126,7 @@ data Equal : forall a, b . a -> b -> Type where
 
 %name Equal prf
 
-infix 6 ===, ~=~
+export infix 6 ===, ~=~
 
 -- An equality type for when you want to assert that each side of the
 -- equality has the same type, but there's not other evidence available
diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr
index dc5be05612..12622d2574 100644
--- a/libs/prelude/Prelude/Basics.idr
+++ b/libs/prelude/Prelude/Basics.idr
@@ -69,7 +69,7 @@ public export %tcinline
 on : (b -> b -> c) -> (a -> b) -> a -> a -> c
 on f g = \x, y => g x `f` g y
 
-infixl 0 `on`
+export infixl 0 `on`
 
 ||| Takes in the first two arguments in reverse order.
 ||| @ f the function to flip
diff --git a/libs/prelude/Prelude/Ops.idr b/libs/prelude/Prelude/Ops.idr
index 062b426700..dc987a1b8b 100644
--- a/libs/prelude/Prelude/Ops.idr
+++ b/libs/prelude/Prelude/Ops.idr
@@ -1,30 +1,30 @@
 module Prelude.Ops
 
 -- Numerical operators
-infix 6 ==, /=, <, <=, >, >=
-infixl 8 +, -
-infixl 9 *, /
+export infix 6 ==, /=, <, <=, >, >=
+export infixl 8 +, -
+export infixl 9 *, /
 
 -- Boolean operators
-infixr 5 &&
-infixr 4 ||
+export infixr 5 &&
+export infixr 4 ||
 
 -- List and String operators
-infixr 7 ::, ++
-infixl 7 :<
+export infixr 7 ::, ++
+export infixl 7 :<
 
 -- Equivalence
-infix 0 <=>
+export infix 0 <=>
 
 -- Functor/Applicative/Monad/Algebra operators
-infixl 1 >>=, =<<, >>, >=>, <=<, <&>
-infixr 2 <|>
-infixl 3 <*>, *>, <*
-infixr 4 <$>, $>, <$
-infixl 8 <+>
+export infixl 1 >>=, =<<, >>, >=>, <=<, <&>
+export infixr 2 <|>
+export infixl 3 <*>, *>, <*
+export infixr 4 <$>, $>, <$
+export infixl 8 <+>
 
 -- Utility operators
-infixr 9 ., .:
-infixr 0 $
+export infixr 9 ., .:
+export infixr 0 $
 
-infixl 9 `div`, `mod`
+export infixl 9 `div`, `mod`
diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
index 7482c10e99..95bc08c2c4 100644
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@@ -406,8 +406,8 @@ Ord a => Ord (List a) where
 
 namespace SnocList
 
-  infixl 7 <><
-  infixr 6 <>>
+  export infixl 7 <><
+  export infixr 6 <>>
 
   ||| 'fish': Action of lists on snoc-lists
   public export
diff --git a/src/Algebra/Semiring.idr b/src/Algebra/Semiring.idr
index cbe0b9f0c3..f1fcdca94f 100644
--- a/src/Algebra/Semiring.idr
+++ b/src/Algebra/Semiring.idr
@@ -2,8 +2,8 @@ module Algebra.Semiring
 
 %default total
 
-infixl 8 |+|
-infixl 9 |*|
+export infixl 8 |+|
+export infixl 9 |*|
 
 ||| A Semiring has two binary operations and an identity for each
 public export
diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr
index 20d62bba1d..fedb7dbef2 100644
--- a/src/Core/Hash.idr
+++ b/src/Core/Hash.idr
@@ -23,7 +23,7 @@ interface Hashable a where
   hash = hashWithSalt 5381
   hashWithSalt h i = h * 33 + hash i
 
-infixl 5 `hashWithSalt`
+export infixl 5 `hashWithSalt`
 
 export
 Hashable Int where
diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr
index 1ef73ff554..1f081303fc 100644
--- a/src/Idris/Doc/Keywords.idr
+++ b/src/Idris/Doc/Keywords.idr
@@ -12,7 +12,8 @@ import Libraries.Data.List.Quantifiers.Extra
 import Libraries.Data.String.Extra
 
 
-infix 10 ::=
+private infix 10 ::=
+
 data DocFor : String -> Type where
   (::=) : (0 str : String) -> (doc : Doc IdrisDocAnn) -> DocFor str
 
diff --git a/src/Libraries/Data/Ordering/Extra.idr b/src/Libraries/Data/Ordering/Extra.idr
index 1e00a524a8..f9691042c7 100644
--- a/src/Libraries/Data/Ordering/Extra.idr
+++ b/src/Libraries/Data/Ordering/Extra.idr
@@ -2,7 +2,7 @@ module Libraries.Data.Ordering.Extra
 
 %default total
 
-infixl 5 `thenCmp`
+export infixl 5 `thenCmp`
 
 export
 thenCmp : Ordering -> Lazy Ordering -> Ordering
diff --git a/src/Libraries/Data/PosMap.idr b/src/Libraries/Data/PosMap.idr
index 00dbdf6866..d38b46dd42 100644
--- a/src/Libraries/Data/PosMap.idr
+++ b/src/Libraries/Data/PosMap.idr
@@ -12,8 +12,8 @@ import Data.List
 
 %default total
 
-infixr 5 <|, <:
-infixl 5 |>, :>
+export infixr 5 <|, <:
+export infixl 5 |>, :>
 
 public export
 FileRange : Type
diff --git a/src/Libraries/Data/String/Extra.idr b/src/Libraries/Data/String/Extra.idr
index ece2ad214b..6a6dea930e 100644
--- a/src/Libraries/Data/String/Extra.idr
+++ b/src/Libraries/Data/String/Extra.idr
@@ -7,8 +7,8 @@ import Data.String
 
 %default total
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 ||| Adds a character to the end of the specified string.
 |||
diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr
index a3e9ef7ca5..adb8080248 100644
--- a/src/Libraries/Text/Parser/Core.idr
+++ b/src/Libraries/Text/Parser/Core.idr
@@ -132,7 +132,7 @@ export %inline
         Grammar state tok (c1 && c2) ty
 (<|>) = Alt
 
-infixr 2 <||>
+export infixr 2 <||>
 ||| Take the tagged disjunction of two grammars. If both consume, the
 ||| combination is guaranteed to consume.
 export
diff --git a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
index d74599e3f7..61e39077bd 100644
--- a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
+++ b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
@@ -134,7 +134,7 @@ export
 fill : Int -> Doc ann -> Doc ann
 fill n doc = width doc (\w => spaces $ n - w)
 
-infixr 6 <++>
+export infixr 6 <++>
 ||| Concatenates two documents with a space in between.
 export
 (<++>) : Doc ann -> Doc ann -> Doc ann
diff --git a/src/Libraries/Utils/Path.idr b/src/Libraries/Utils/Path.idr
index 8966437385..7a148dc4ef 100644
--- a/src/Libraries/Utils/Path.idr
+++ b/src/Libraries/Utils/Path.idr
@@ -19,9 +19,9 @@ import System.File
 
 %default total
 
-infixl 5 </>, />
-infixr 7 <.>
-infixr 7 <..>
+export infixl 5 </>, />
+export infixr 7 <.>
+export infixr 7 <..>
 
 
 ||| The character that separates directories in the path.