diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index 1c237367f..ee8ca0727 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -30,6 +30,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   customise the syntax of operator to look more like a binder.
   See [#3113](https://github.com/idris-lang/Idris2/issues/3113).
 
+* Fixity declarations without an export modifier now emit a warning in peparation
+  for a future version where they will become private by default.
+
 * Elaborator scripts were made to be able to access the visibility modifier of a
   definition, via `getVis`.
 
diff --git a/libs/base/Data/Bits.idr b/libs/base/Data/Bits.idr
index 68bc156cb..0d3ce45e1 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 b0d441b6e..098d66a42 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/Fin.idr b/libs/base/Data/Fin.idr
index 009fa32ca..997b5c65b 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -304,7 +304,7 @@ namespace Equality
     FZ : Pointwise FZ FZ
     FS : Pointwise k l -> Pointwise (FS k) (FS l)
 
-  infix 6 ~~~
+  export infix 6 ~~~
   ||| Convenient infix notation for the notion of pointwise equality of Fins
   public export
   (~~~) : Fin m -> Fin n -> Type
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index edc1d16da..e879de24e 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 1b02fb5cb..072ad9268 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 d25c2c010..9b0cb356b 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 c4ee8f47e..75c72114a 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 e5ab95998..82e429fda 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 b52f71ba4..2f7732269 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 000000000..ae3cc8ea9
--- /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 0250fe775..0b4a920a4 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 f8d877ffa..6fa1fc9eb 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 13922d3b6..26fe8f12c 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 1c0e72bb8..bf59a96d0 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 00317c787..3357f9aff 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 b80d19aaa..eb62d1ed2 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 d2e44bbb3..f7ddbe386 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 b9cf10664..a54f39c4a 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 43578cbd7..79ca527cc 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 cb0eb28f5..ce011cc97 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 40f45b84a..418bd4746 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 4de6f12f4..bf5b46121 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 88c077320..1d97e6a95 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 d46f308e7..d4dbdc419 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/Syntax/WithProof.idr b/libs/contrib/Syntax/WithProof.idr
index 0c57d4ad8..1231ff535 100644
--- a/libs/contrib/Syntax/WithProof.idr
+++ b/libs/contrib/Syntax/WithProof.idr
@@ -1,6 +1,6 @@
 module Syntax.WithProof
 
-prefix 10 @@
+export prefix 10 @@
 
 ||| Until Idris2 supports the 'with (...) proof p' construct, here's a
 ||| poor-man's replacement.
diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr
index 1b43bd56e..603f6f9bb 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 93db72bb9..2dc7c9812 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 97fb9f7d3..c2ec32d49 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/Copies.idr b/libs/linear/Data/Linear/Copies.idr
index 1fca2dd1f..99a7353b2 100644
--- a/libs/linear/Data/Linear/Copies.idr
+++ b/libs/linear/Data/Linear/Copies.idr
@@ -6,7 +6,7 @@ import Data.Nat
 
 %default total
 
-infix 1 `Copies`
+export infix 1 `Copies`
 
 ||| Carries multiple linear copies of the same value. Usage: m `Copies` x
 ||| reads as "m copies of value x". This data structure is necessary to implement
diff --git a/libs/linear/Data/Linear/Interface.idr b/libs/linear/Data/Linear/Interface.idr
index ec7d857ae..6a8f5fcfe 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 11989ec35..be379a7c6 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
@@ -18,7 +18,7 @@ public export
 (.) : (b -@ c) -@ (a -@ b) -@ (a -@ c)
 (.) f g v = f (g v)
 
-prefix 5 !*
+export prefix 5 !*
 ||| Prefix notation for the linear unrestricted modality
 public export
 record (!*) (a : Type) where
diff --git a/libs/papers/Data/Description/Regular.idr b/libs/papers/Data/Description/Regular.idr
index c4a0251f6..0b904c35b 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 b8dcd4f7a..e92e46ab5 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 c64aa33f5..9539e6c74 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 1e90bd629..1378cbf34 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 2065a9066..6845ca4d3 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 32c2298cb..608916527 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/papers/Search/Tychonoff/PartI.idr b/libs/papers/Search/Tychonoff/PartI.idr
index 1926bcbb5..50c7f5023 100644
--- a/libs/papers/Search/Tychonoff/PartI.idr
+++ b/libs/papers/Search/Tychonoff/PartI.idr
@@ -40,7 +40,7 @@ HilbertEpsilon p = (v : x ** (v0 : x) -> p v0 -> p v)
 0 IsSearchable : Type -> Type
 IsSearchable x = (0 p : Pred x) -> Decidable p -> HilbertEpsilon p
 
-infix 0 <->
+private infix 0 <->
 record (<->) (a, b : Type) where
   constructor MkIso
   forwards  : a -> b
diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr
index 1a839238d..85e778142 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 d275c2c0b..e5b9884d5 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 062b42670..dc987a1b8 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 7482c10e9..95bc08c2c 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 cbe0b9f0c..f1fcdca94 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/Binary.idr b/src/Core/Binary.idr
index 813dd9a96..c967f1f04 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2024_01_23_00
+ttcVersion = 2024_03_29_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 52700615d..c12e21cd2 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -821,9 +821,12 @@ HasNames Error where
   full gam (InRHS fc n err) = InRHS fc <$> full gam n <*> full gam err
   full gam (MaybeMisspelling err xs) = MaybeMisspelling <$> full gam err <*> pure xs
   full gam (WarningAsError wrn) = WarningAsError <$> full gam wrn
-  full gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
+  full gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates)
       = OperatorBindingMismatch {print} fc expected actual
-          <$> full gam opName <*> pure rhs <*> pure candidates
+          <$> (Left <$> full gam opName) <*> pure rhs <*> pure candidates
+  full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
+      = OperatorBindingMismatch {print} fc expected actual
+          <$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates
 
   resolved gam (Fatal err) = Fatal <$> resolved gam err
   resolved _ (CantConvert fc gam rho s t)
@@ -916,9 +919,12 @@ HasNames Error where
   resolved gam (InRHS fc n err) = InRHS fc <$> resolved gam n <*> resolved gam err
   resolved gam (MaybeMisspelling err xs) = MaybeMisspelling <$> resolved gam err <*> pure xs
   resolved gam (WarningAsError wrn) = WarningAsError <$> resolved gam wrn
-  resolved gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
+  resolved gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates)
       = OperatorBindingMismatch {print} fc expected actual
-          <$> resolved gam opName <*> pure rhs <*> pure candidates
+          <$> (Left <$> resolved gam opName) <*> pure rhs <*> pure candidates
+  resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
+      = OperatorBindingMismatch {print} fc expected actual
+          <$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates
 
 export
 HasNames Totality where
diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index 8eaa16b60..29a282741 100644
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@@ -165,8 +165,9 @@ data Error : Type where
      GenericMsg : FC -> String -> Error
      GenericMsgSol : FC -> (message : String) -> (solutions : List String) -> Error
      OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} ->
-         FC -> (expectedFixity : BacktickOrOperatorFixity) -> (use_site : OperatorLHSInfo a) ->
-         (opName : Name) -> (rhs : a) -> (candidates : List String) -> Error
+         FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) ->
+         -- left: backticked, right: op symbolds
+         (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
      CantFindPackage : String -> Error
@@ -403,7 +404,7 @@ Show Error where
   show (OperatorBindingMismatch fc (DeclaredFixity expected) actual opName rhs _)
        = show fc ++ ": Operator " ++ show opName ++ " is " ++ show expected
        ++ " but used as a " ++ show actual ++ " operator"
-  show (OperatorBindingMismatch fc Backticked actual opName rhs _)
+  show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _)
        = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
        ++ " but used as a " ++ show actual ++ " operator"
 
diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr
index 20d62bba1..fedb7dbef 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/Core/TT.idr b/src/Core/TT.idr
index cab8c5323..efa8521ac 100644
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@@ -170,11 +170,11 @@ Eq FixityInfo where
 
 ||| Whenever we read an operator from the parser, we don't know if it's a backticked expression with no fixity
 ||| declaration, or if it has a fixity declaration. If it does not have a declaration, we represent this state
-||| with `Backticked`.
+||| with `UndeclaredFixity`.
 ||| Note that a backticked expression can have a fixity declaration, in which case it is represented with
 ||| `DeclaredFixity`.
 public export
-data BacktickOrOperatorFixity = Backticked | DeclaredFixity FixityInfo
+data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo
 
 -- Left-hand-side information for operators, carries autobind information
 -- an operator can either be
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index a61fd910e..fe32b9540 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -35,6 +35,7 @@ import TTImp.TTImp
 import TTImp.Utils
 
 import Libraries.Data.IMaybe
+import Libraries.Data.WithDefault
 import Libraries.Utils.Shunting
 import Libraries.Text.PrettyPrint.Prettyprinter
 
@@ -106,12 +107,12 @@ mkPrec Infix  = NonAssoc
 mkPrec Prefix = Prefix
 
 -- This is used to print the error message for fixities
-[interpName] Interpolation ((Name, BacktickOrOperatorFixity), b) where
-  interpolate ((x, _), _) = show x
+[interpName] Interpolation ((OpStr' Name, FixityDeclarationInfo), b) where
+  interpolate ((x, _), _) = show x.toName
 
-[showWithLoc] Show ((Name, BacktickOrOperatorFixity), b) where
+[showWithLoc] Show ((OpStr' Name, FixityDeclarationInfo), b) where
   show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc
-  show ((x, Backticked), _) = show x
+  show ((x, UndeclaredFixity), _) = show x
 
 -- Check that an operator does not have any conflicting fixities in scope.
 -- Each operator can have its fixity defined multiple times across multiple
@@ -121,19 +122,19 @@ mkPrec Prefix = Prefix
 checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} ->
                            {auto c : Ref Ctxt Defs} ->
                            (isPrefix : Bool) ->
-                           FC -> Name -> Core (OpPrec, BacktickOrOperatorFixity)
+                           FC -> OpStr' Name -> Core (OpPrec, FixityDeclarationInfo)
 checkConflictingFixities isPrefix exprFC opn
-  = do let op = nameRoot opn
+  = do let op = nameRoot opn.toName
        foundFixities <- getFixityInfo op
        let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities
        case (isPrefix, pre, inf) of
-            -- If we do not find any fixity for this operator we check that it uses operator
-            -- characters, if not, it must be a backticked expression.
-            (_, [], []) => if any isOpChar (fastUnpack op)
-                              then throw (GenericMsg exprFC "Unknown operator '\{op}'")
-                              else pure (NonAssoc 1, Backticked) -- Backticks are non associative by default
+            -- If we do not find any fixity, and it is a backticked operator, then we
+            -- return the default fixity and associativity for backticked operators
+            -- Otherwise, it's an unknown operator.
+            (_, [], []) => case opn of
+                              OpSymbols _ => throw (GenericMsg exprFC "Unknown operator '\{op}'")
+                              Backticked _ =>  pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default
 
-            --
             (True, ((fxName, fx) :: _), _) => do
                 -- in the prefix case, remove conflicts with infix (-)
                 let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf)
@@ -171,17 +172,18 @@ checkConflictingFixities isPrefix exprFC opn
 
 checkConflictingBinding : Ref Ctxt Defs =>
                           Ref Syn SyntaxInfo =>
-                          FC -> Name -> (foundFixity : BacktickOrOperatorFixity) ->
+                          FC -> OpStr -> (foundFixity : FixityDeclarationInfo) ->
                           (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
 checkConflictingBinding fc opName foundFixity use_site rhs
     = if isCompatible foundFixity use_site
          then pure ()
          else throw $ OperatorBindingMismatch
-             {print = byShow} fc foundFixity use_site opName rhs !candidates
+             {print = byShow} fc foundFixity use_site (opNameToEither opName) rhs !candidates
     where
-      isCompatible : BacktickOrOperatorFixity -> OperatorLHSInfo PTerm -> Bool
-      isCompatible Backticked (NoBinder lhs) = True
-      isCompatible Backticked _ = False
+
+      isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
+      isCompatible UndeclaredFixity (NoBinder lhs) = True
+      isCompatible UndeclaredFixity _ = False
       isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo.bindingInfo == NotBinding
       isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo.bindingInfo == Typebind
       isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo.bindingInfo == Autobind
@@ -198,10 +200,10 @@ checkConflictingBinding fc opName foundFixity use_site rhs
       candidates = do let DeclaredFixity fxInfo = foundFixity
                         | _ => pure [] -- if there is no declared fixity we can't know what's
                                        -- supposed to go there.
-                      Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName
+                      Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName.toName
                         | Nothing => pure []
                       ns <- currentNS <$> get Ctxt
-                      pure (showSimilarNames ns opName nm cs)
+                      pure (showSimilarNames ns opName.toName nm cs)
 
 checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool
 
@@ -225,7 +227,7 @@ checkValidFixity _ _ _ = False
 parameters (side : Side)
   toTokList : {auto s : Ref Syn SyntaxInfo} ->
               {auto c : Ref Ctxt Defs} ->
-              PTerm -> Core (List (Tok ((OpStr, BacktickOrOperatorFixity), Maybe (OperatorLHSInfo PTerm)) PTerm))
+              PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm))
   toTokList (POp fc opFC l opn r)
       = do (precInfo, fixInfo) <- checkConflictingFixities False fc opn
            unless (side == LHS) -- do not check for conflicting fixity on the LHS
@@ -393,7 +395,7 @@ mutual
       = do syn <- get Syn
            -- It might actually be a prefix argument rather than a section
            -- so check that first, otherwise desugar as a lambda
-           case lookupName op (prefixes syn) of
+           case lookupName op.toName (prefixes syn) of
                 [] =>
                     desugarB side ps
                         (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
@@ -798,10 +800,10 @@ mutual
                 {auto o : Ref ROpts REPLOpts} ->
                 Side -> List Name -> Tree (OpStr, Maybe $ OperatorLHSInfo PTerm) PTerm ->
                 Core PTerm
-  desugarTree side ps (Infix loc eqFC (UN $ Basic "=", _) l r) -- special case since '=' is special syntax
+  desugarTree side ps (Infix loc eqFC (OpSymbols $ UN $ Basic "=", _) l r) -- special case since '=' is special syntax
       = pure $ PEq eqFC !(desugarTree side ps l) !(desugarTree side ps r)
 
-  desugarTree side ps (Infix loc _ (UN $ Basic "$", _) l r) -- special case since '$' is special syntax
+  desugarTree side ps (Infix loc _ (OpSymbols $ UN $ Basic "$", _) l r) -- special case since '$' is special syntax
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r
            pure (PApp loc l' r')
@@ -809,25 +811,25 @@ mutual
   desugarTree side ps (Infix loc opFC (op, Just (NoBinder lhs)) l r)
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r
-           pure (PApp loc (PApp loc (PRef opFC op) l') r')
+           pure (PApp loc (PApp loc (PRef opFC op.toName) l') r')
   -- (x : ty) =@ f x ==>> (=@) ty (\x : ty => f x)
   desugarTree side ps (Infix loc opFC (op, Just (BindType pat lhs)) l r)
       = do l' <- desugarTree side ps l
            body <- desugarTree side ps r
-           pure $ PApp loc (PApp loc (PRef opFC op) l')
+           pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
                       (PLam loc top Explicit pat l' body)
   -- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x)
   desugarTree side ps (Infix loc opFC (op, Just (BindExpr pat lhs)) l r)
       = do l' <- desugarTree side ps l
            body <- desugarTree side ps r
-           pure $ PApp loc (PApp loc (PRef opFC op) l')
+           pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
                       (PLam loc top Explicit pat (PInfer opFC) body)
 
   -- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x)
   desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType pat ty expr)) l r)
       = do l' <- desugarTree side ps l
            body <- desugarTree side ps r
-           pure $ PApp loc (PApp loc (PRef opFC op) l')
+           pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
                       (PLam loc top Explicit pat ty body)
   desugarTree side ps (Infix loc opFC (op, Nothing) _ r)
       = throw $ InternalError "illegal fixity: Parsed as infix but no binding information"
@@ -838,7 +840,7 @@ mutual
   -- Note: In case of negated signed integer literals, we apply the
   -- negation directly. Otherwise, the literal might be
   -- truncated to 0 before being passed on to `negate`.
-  desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) $ Leaf $ PPrimVal fc c)
+  desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) $ Leaf $ PPrimVal fc c)
     = let newFC    = fromMaybe EmptyFC (mergeFC loc fc)
           continue = desugarTree side ps . Leaf . PPrimVal newFC
        in case c of
@@ -854,13 +856,13 @@ mutual
             _     => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c)
                         pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')
 
-  desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) arg)
+  desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) arg)
     = do arg' <- desugarTree side ps arg
          pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')
 
   desugarTree side ps (Pre loc opFC (op, _) arg)
       = do arg' <- desugarTree side ps arg
-           pure (PApp loc (PRef opFC op) arg')
+           pure (PApp loc (PRef opFC op.toName) arg')
   desugarTree side ps (Leaf t) = pure t
 
   desugarType : {auto s : Ref Syn SyntaxInfo} ->
@@ -1016,6 +1018,11 @@ mutual
                      List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
   mapDesugarPiInfo ps = PiInfo.traverse (desugar AnyExpr ps)
 
+  displayFixity : Maybe Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> String
+  displayFixity Nothing NotBinding fix prec op = "\{show fix} \{show  prec} \{show op}"
+  displayFixity Nothing bind fix prec op = "\{show bind} \{show fix} \{show  prec} \{show op}"
+  displayFixity (Just vis) bind fix prec op = "\{show vis} \{show bind} \{show fix} \{show  prec} \{show op}"
+
   -- Given a high level declaration, return a list of TTImp declarations
   -- which process it, and update any necessary state on the way.
   export
@@ -1205,22 +1212,35 @@ mutual
           NS ns (DN str (MN ("__mk" ++ str) 0))
       mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
 
-  desugarDecl ps (PFixity fc vis binding fix prec opName)
+  desugarDecl ps fx@(PFixity fc vis binding fix prec opName)
       = do unless (checkValidFixity binding fix prec)
              (throw $ GenericMsgSol fc
                  "Invalid fixity, \{binding} operator must be infixr 0."
                  [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`"
                  , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`"
                  ])
+           when (isDefaulted vis) $
+             let adjustedExport = displayFixity (Just Export) binding fix prec opName
+                 adjustedPrivate = displayFixity (Just Private) binding fix prec opName
+                 originalFixity = displayFixity Nothing binding fix prec opName
+             in recordWarning $ GenericWarn fc """
+               Fixity declaration '\{originalFixity}' does not have an export modifier, and
+               will become private by default in a future version.
+               To expose it outside of its module, write '\{adjustedExport}'. If you
+               intend to keep it private, write '\{adjustedPrivate}'.
+               """
            ctx <- get Ctxt
            -- We update the context of fixities by adding a namespaced fixity
            -- given by the current namespace and its fixity name.
            -- This allows fixities to be stored along with the namespace at their
            -- declaration site and detect and handle ambiguous fixities
            let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix))
-                              (UN $ Basic $ nameRoot opName)
+                              (UN $ Basic $ nameRoot opName.toName)
 
-           update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis binding fix prec) }
+           update Syn
+             { fixities $=
+               addName updatedNS
+                 (MkFixityInfo fc (collapseDefault vis) binding fix prec) }
            pure []
   desugarDecl ps d@(PFail fc mmsg ds)
       = do -- save the state: the content of a failing block should be discarded
diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr
index 1ef73ff55..1f081303f 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/Idris/Error.idr b/src/Idris/Error.idr
index f26c6dc49..a8fd7e1cc 100644
--- a/src/Idris/Error.idr
+++ b/src/Idris/Error.idr
@@ -14,6 +14,7 @@ import Idris.Pretty
 import Parser.Source
 
 import Data.List
+import Data.Either
 import Data.List1
 import Data.String
 
@@ -626,14 +627,14 @@ perrorRaw (GenericMsgSol fc header solutions)
        <+> "Possible solutions:" <+> line
        <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions))
 perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates)
-    = pure $ "Operator" <++> pretty0 !(getFullName opName) <++> "is"
-       <++> printBindingInfo expected
+    = pure $ "Operator" <++> pretty0 !(getFullName (fromEither opName)) <++> "is"
+       <++> printBindingInfo expected-- .bindingInfo
        <++> "operator, but is used as" <++> printBindingModifier actual.getBinder
        <++> "operator."
        <+> line <+> !(ploc fc)
        <+> "Explanation: regular, typebind and autobind operators all use a slightly different"
-       <++> "syntax, typebind looks like this: '(name : type)" <++> pretty0 opName
-       <++> "expr', autobind looks like this: '(name := expr)" <++> pretty0 opName
+       <++> "syntax, typebind looks like this: '(name : type)" <++> infixOpName
+       <++> "expr', autobind looks like this: '(name := expr)" <++> infixOpName
        <++> "expr'."
        <+> line <+> line
        <+> "Possible solutions:" <+> line
@@ -650,45 +651,46 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi
 
       moduleDiagnostic : Doc IdrisAnn
       moduleDiagnostic = case expected of
-                              Backticked => "Import a module that exports a suitable fixity."
-                              (DeclaredFixity a) => "Hide or remove the fixity at" <++> byShow a.fc
-                                     <++> "and import a module that exports a compatible fixity."
+                              UndeclaredFixity => "Import a module that exports a suitable fixity."
+                              (DeclaredFixity e) => "Hide or remove the fixity at" <++> byShow e.fc
+                                  <++> "and import a module that exports a compatible fixity."
+
       infixOpName : Doc IdrisAnn
-      infixOpName = case expected of
-                         Backticked => enclose "`" "`" (byShow opName)
-                         _ => byShow opName
+      infixOpName = case opName of
+                         Left backtickedOp => enclose "`" "`" (byShow backtickedOp)
+                         Right symbolOp => byShow symbolOp
 
       displayFixityInfo : FixityInfo -> BindingModifier -> Doc IdrisAnn
       displayFixityInfo (MkFixityInfo fc1 vis _ fix precedence) NotBinding
-        = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 opName
+        = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 (fromEither opName)
       displayFixityInfo (MkFixityInfo _ vis _ fix precedence) usedBinder
-        = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 opName
+        = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 (fromEither opName)
 
       printE : ? -> Doc IdrisAnn
       printE x = reAnnotate (const Code) (p x)
 
       expressionDiagnositc : List (Doc IdrisAnn)
       expressionDiagnositc = case expected of
-          Backticked => []
-          (DeclaredFixity e) => let sentence = "Write the expression using" <++> byShow e.bindingInfo <++> "syntax:"
-                   in pure $ sentence <++> enclose "'" "'" (case e.bindingInfo of
-                           NotBinding =>
-                              printE actual.getLhs <++> infixOpName <++> printE rhs
-                           Autobind =>
-                              parens (maybe "_" printE actual.getBoundPat <++> ":="
-                                      <++> printE actual.getLhs)
-                              <++> infixOpName <++> printE rhs
-                           Typebind =>
-                              parens (maybe "_" printE actual.getBoundPat <++> ":"
-                                      <++> printE actual.getLhs)
-                              <++> infixOpName <++> printE rhs
-                           ) <+> dot
+          UndeclaredFixity => []
+          DeclaredFixity e => let sentence = "Write the expression using" <++> byShow e.bindingInfo <++> "syntax:"
+            in pure $ sentence <++> enclose "'" "'" (case e.bindingInfo of
+                    NotBinding =>
+                       printE actual.getLhs <++> infixOpName <++> printE rhs
+                    Autobind =>
+                       parens (maybe "_" printE actual.getBoundPat <++> ":="
+                               <++> printE actual.getLhs)
+                       <++> infixOpName <++> printE rhs
+                    Typebind =>
+                       parens (maybe "_" printE actual.getBoundPat <++> ":"
+                               <++> printE actual.getLhs)
+                       <++> infixOpName <++> printE rhs
+                    ) <+> dot
 
 
       fixityDiagnostic : Doc IdrisAnn
       fixityDiagnostic = case expected of
-          Backticked => "Define a new fixity:" <++> "infixr 0" <++> infixOpName
-          (DeclaredFixity fix) =>
+           UndeclaredFixity => "Define a new fixity:" <++> "infixr 0" <++> infixOpName
+           (DeclaredFixity fix) =>
             "Change the fixity defined at" <++> pretty0 fix.fc <++> "to"
             <++> enclose "'" "'" (displayFixityInfo fix actual.getBinder)
             <+> dot
@@ -698,8 +700,8 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi
       printBindingModifier Typebind = "a type-binding (typebind)"
       printBindingModifier Autobind = "an automatically-binding (autobind)"
 
-      printBindingInfo : BacktickOrOperatorFixity -> Doc IdrisAnn
-      printBindingInfo Backticked = "a regular"
+      printBindingInfo : FixityDeclarationInfo -> Doc IdrisAnn
+      printBindingInfo UndeclaredFixity = "a regular"
       printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo
 
 
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index e8910f52f..0be4fc526 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -176,9 +176,10 @@ continueWith : IndentInfo -> String -> Rule ()
 continueWith indents req
     = mustContinue indents (Just req) *> symbol req
 
-iOperator : Rule Name
+iOperator : Rule OpStr
 iOperator
-    = operator <|> (symbol "`" *> name <* symbol "`")
+    = OpSymbols <$> operator
+  <|> Backticked <$> (symbol "`" *> name <* symbol "`")
 
 data ArgType
     = UnnamedExpArg PTerm
@@ -369,14 +370,14 @@ mutual
                        pure $
                          let fc = boundToFC fname (mergeBounds l r)
                              opFC = virtualiseFC fc -- already been highlighted: we don't care
-                         in POp fc opFC (NoBinder l.val) (UN $ Basic "=") r.val
+                         in POp fc opFC (NoBinder l.val) (OpSymbols $ UN $ Basic "=") r.val
                else fail "= not allowed")
              <|>
              (do b <- bounds $ do
                         continue indents
                         op <- bounds iOperator
                         e <- case op.val of
-                               UN (Basic "$") => typeExpr q fname indents
+                               OpSymbols (UN (Basic "$")) => typeExpr q fname indents
                                _ => expr q fname indents
                         pure (op, e)
                  (op, r) <- pure b.val
@@ -1175,10 +1176,10 @@ visibility fname
     = (specified <$> visOption fname)
   <|> pure defaulted
 
-exportVisibility : OriginDesc -> EmptyRule Visibility
+exportVisibility : OriginDesc -> EmptyRule (WithDefault Visibility Export)
 exportVisibility fname
-    = visOption fname
-  <|> pure Export
+    = (specified <$> visOption fname)
+  <|> pure defaulted
 
 tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule (List1 PTypeDecl)
 tyDecls declName predoc fname indents
diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr
index 34f0eb421..ee44d85cd 100644
--- a/src/Idris/Pretty.idr
+++ b/src/Idris/Pretty.idr
@@ -334,24 +334,24 @@ mutual
     prettyPrec d (PInfer _) = annotate Hole $ "?"
     prettyPrec d (POp _ _ (BindType nm left) op right) =
         group $ parens (prettyPrec d nm <++> ":" <++> pretty left)
-           <++> prettyOp op
+           <++> prettyOp op.toName
            <++> pretty right
     prettyPrec d (POp _ _ (BindExpr nm left) op right) =
         group $ parens (prettyPrec d nm <++> ":=" <++> pretty left)
-           <++> prettyOp op
+           <++> prettyOp op.toName
            <++> pretty right
     prettyPrec d (POp _ _ (BindExplicitType nm ty left) op right) =
         group $ parens (prettyPrec d nm <++> ":" <++> pretty ty <++> ":=" <++> pretty left)
-           <++> prettyOp op
+           <++> prettyOp op.toName
            <++> pretty right
     prettyPrec d (POp _ _ (NoBinder x) op y) =
       parenthesise (d >= App) $
         group $ pretty x
-           <++> prettyOp op
+           <++> prettyOp op.toName
            <++> pretty y
-    prettyPrec d (PPrefixOp _ _ op x) = parenthesise (d > startPrec) $ prettyOp op <+> pretty x
-    prettyPrec d (PSectionL _ _ op x) = parens (prettyOp op <++> pretty x)
-    prettyPrec d (PSectionR _ _ x op) = parens (pretty x <++> prettyOp op)
+    prettyPrec d (PPrefixOp _ _ op x) = parenthesise (d > startPrec) $ prettyOp op.toName <+> pretty x
+    prettyPrec d (PSectionL _ _ op x) = parens (prettyOp op.toName <++> pretty x)
+    prettyPrec d (PSectionR _ _ x op) = parens (pretty x <++> prettyOp op.toName)
     prettyPrec d (PEq fc l r) = parenthesise (d > startPrec) $ prettyPrec Equal l <++> equals <++> prettyPrec Equal r
     prettyPrec d (PBracketed _ tm) = parens (pretty tm)
     prettyPrec d (PString _ _ xs) = parenthesise (d > startPrec) $ hsep $ punctuate "++" (prettyPStr <$> xs)
diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr
index 2f0607ba0..cc39c7f4f 100644
--- a/src/Idris/Resugar.idr
+++ b/src/Idris/Resugar.idr
@@ -46,7 +46,7 @@ mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)
        -- to know if the name is an operator or not, it's enough to check
        -- that the fixity context contains the name `(++)`
        let rootName = UN (Basic (nameRoot raw))
-       let asOp = POp fc opFC (NoBinder (unbracketApp x)) kn (unbracketApp y)
+       let asOp = POp fc opFC (NoBinder (unbracketApp x)) (OpSymbols kn) (unbracketApp y)
        if not (null (lookupName rootName (infixes syn)))
          then pure asOp
          else case dropNS raw of
@@ -55,7 +55,7 @@ mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)
 mkOp tm@(PApp fc (PRef opFC kn) x)
   = do syn <- get Syn
        let n = rawName kn
-       let asOp = PSectionR fc opFC (unbracketApp x) kn
+       let asOp = PSectionR fc opFC (unbracketApp x) (OpSymbols kn)
        if not (null $ lookupName (UN $ Basic (nameRoot n)) (infixes syn))
          then pure asOp
          else case dropNS n of
@@ -73,7 +73,7 @@ mkSectionL tm@(PLam fc rig info (PRef _ bd) ty
          | _ => pure tm
        syn <- get Syn
        let n = rawName kn
-       let asOp = PSectionL fc opFC kn (unbracketApp x)
+       let asOp = PSectionL fc opFC (OpSymbols kn) (unbracketApp x)
        if not (null $ lookupName (UN $ Basic (nameRoot n)) (fixities syn))
          then pure asOp
          else case dropNS n of
@@ -591,15 +591,15 @@ cleanPTerm ptm
     cleanNode (PRef fc nm)    =
       PRef fc <$> cleanKindedName nm
     cleanNode (POp fc opFC abi op y) =
-      (\ op => POp fc opFC abi op y) <$> cleanKindedName op
+      (\ op => POp fc opFC abi op y) <$> traverseOp @{Functor.CORE} cleanKindedName op
     cleanNode (PPrefixOp fc opFC op x) =
-      (\ op => PPrefixOp fc opFC op x) <$> cleanKindedName op
+      (\ op => PPrefixOp fc opFC op x) <$> traverseOp @{Functor.CORE} cleanKindedName op
     cleanNode (PSectionL fc opFC op x) =
-      (\ op => PSectionL fc opFC op x) <$> cleanKindedName op
+      (\ op => PSectionL fc opFC op x) <$> traverseOp @{Functor.CORE} cleanKindedName op
     cleanNode (PSectionR fc opFC x op) =
-      PSectionR fc opFC x <$> cleanKindedName op
+      PSectionR fc opFC x <$> traverseOp @{Functor.CORE} cleanKindedName op
     cleanNode (PPi fc rig vis (Just n) arg ret) =
-      (\ n => PPi fc rig vis n arg ret) <$> cleanBinderName vis n
+      (\ n => PPi fc rig vis n arg ret) <$> (cleanBinderName vis n)
     cleanNode tm = pure tm
 
 toCleanPTerm : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 56bd1b7c4..b09b3e5fd 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -30,8 +30,39 @@ import Parser.Lexer.Source
 %default covering
 
 public export
-OpStr' : Type -> Type
-OpStr' nm = nm
+data OpStr' nm = OpSymbols nm | Backticked nm
+
+-- Left: backticked, Right: operator symbols
+export
+opNameToEither : OpStr' nm -> Either nm nm
+opNameToEither (Backticked nm) = Left nm
+opNameToEither (OpSymbols nm) = Right nm
+
+export
+Functor OpStr' where
+  map f (OpSymbols x) = OpSymbols (f x)
+  map f (Backticked x) = Backticked (f x)
+
+export
+Foldable OpStr' where
+  foldr f i (OpSymbols x) = f x i
+  foldr f i (Backticked x) = f x i
+
+export
+traverseOp : (fn : Functor f) => (a -> f b) -> OpStr' a -> f (OpStr' b)
+traverseOp f (OpSymbols x) = map OpSymbols (f x)
+traverseOp f (Backticked x) = map Backticked (f x)
+
+
+public export
+Show nm => Show (OpStr' nm) where
+  show (OpSymbols nm) = show nm
+  show (Backticked nm) = "`\{show nm}`"
+
+public export
+(.toName) : OpStr' nm -> nm
+(.toName) (OpSymbols nm) = nm
+(.toName) (Backticked nm) = nm
 
 public export
 OpStr : Type
@@ -434,7 +465,7 @@ mutual
        PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm
 
        PMutual : FC -> List (PDecl' nm) -> PDecl' nm
-       PFixity : FC -> Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> PDecl' nm
+       PFixity : FC -> WithDefault Visibility Export -> BindingModifier -> Fixity -> Nat -> OpStr -> PDecl' nm
        PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm
        PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm
        PRunElabDecl : FC -> PTerm' nm -> PDecl' nm
@@ -832,10 +863,8 @@ parameters {0 nm : Type} (toName : nm -> Name)
   showPTermPrec d (PWithUnambigNames fc ns rhs)
         = "with " ++ show ns ++ " " ++ showPTermPrec d rhs
 
-  showOpPrec d op = let op = toName op in
-    if isOpName op
-    then        showPrec d op
-    else "`" ++ showPrec d op ++ "`"
+  showOpPrec d (OpSymbols op) = showPrec d (toName op)
+  showOpPrec d (Backticked op) = "`\{showPrec d (toName op)}`"
 
 export
 covering
@@ -1045,3 +1074,4 @@ Show PDecl where
   show (PRunElabDecl{}) = "PRunElabDecl"
   show (PDirective{}) = "PDirective"
   show (PBuiltin{}) = "PBuiltin"
+
diff --git a/src/Idris/Syntax/Views.idr b/src/Idris/Syntax/Views.idr
index 34e9de748..c10612e46 100644
--- a/src/Idris/Syntax/Views.idr
+++ b/src/Idris/Syntax/Views.idr
@@ -27,7 +27,7 @@ getFnArgs embed fts = go fts [] where
   go (PNamedApp fc f n t) = go f . (Named fc n t ::)
   go (PBracketed fc f) = go f
   -- we don't care about the binder info here
-  go (POp fc opFC leftSide op r) = (PRef opFC op,) . (Explicit fc leftSide.getLhs ::) . (Explicit fc r ::)
+  go (POp fc opFC leftSide op r) = (PRef opFC op.toName,) . (Explicit fc leftSide.getLhs ::) . (Explicit fc r ::)
   go (PEq fc l r) = (PRef fc $ embed eqName,) . (Explicit fc l ::) . (Explicit fc r ::)
   -- ambiguous, picking the type constructor here
   go (PPair fc l r) = (PRef fc $ embed pairname,) . (Explicit fc l ::) . (Explicit fc r ::)
diff --git a/src/Libraries/Data/Ordering/Extra.idr b/src/Libraries/Data/Ordering/Extra.idr
index 1e00a524a..f9691042c 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 00dbdf686..d38b46dd4 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 ece2ad214..6a6dea930 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 a3e9ef7ca..adb808024 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 d74599e3f..61e39077b 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 896643738..7a148dc4e 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.
diff --git a/tests/base/sortedmap_001/SortedMapTest.idr b/tests/base/sortedmap_001/SortedMapTest.idr
index c6222f5b8..cc107e867 100644
--- a/tests/base/sortedmap_001/SortedMapTest.idr
+++ b/tests/base/sortedmap_001/SortedMapTest.idr
@@ -3,7 +3,7 @@ import Data.SortedMap
 (&~) : a -> (a -> b) -> b
 (&~) x f = f x
 
-infixl 2 &~
+private infixl 2 &~
 
 testLookupBetween : List (Maybe (Maybe (Int,Int),Maybe (Int,Int)))
 testLookupBetween =
diff --git a/tests/ideMode/ideMode005/LetBinders.idr b/tests/ideMode/ideMode005/LetBinders.idr
index ac8a898bf..40ed1e683 100644
--- a/tests/ideMode/ideMode005/LetBinders.idr
+++ b/tests/ideMode/ideMode005/LetBinders.idr
@@ -1,6 +1,6 @@
 module LetBinders
 
-infix 1 :::
+private infix 1 :::
 record List1 (a : Type) where
   constructor (:::)
   head : a
diff --git a/tests/ideMode/ideMode005/expectedG b/tests/ideMode/ideMode005/expectedG
index 4b8df8d28..f7bbd2dde 100644
--- a/tests/ideMode/ideMode005/expectedG
+++ b/tests/ideMode/ideMode005/expectedG
@@ -2,8 +2,9 @@
 00003e(:write-string "1/1: Building LetBinders (LetBinders.idr)" 1)
 000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 0 0) (:end 0 6)) ((:decor :keyword)))))) 1)
 000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 0 7) (:end 0 17)) ((:decor :module)))))) 1)
-000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 0) (:end 2 5)) ((:decor :keyword)))))) 1)
-000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 6) (:end 2 7)) ((:decor :keyword)))))) 1)
+000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 0) (:end 2 7)) ((:decor :keyword)))))) 1)
+000076(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 8) (:end 2 13)) ((:decor :keyword)))))) 1)
+000077(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 2 14) (:end 2 15)) ((:decor :keyword)))))) 1)
 000075(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 3 0) (:end 3 6)) ((:decor :keyword)))))) 1)
 000073(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 3 7) (:end 3 12)) ((:decor :type)))))) 1)
 000077(:output (:ok (:highlight-source ((((:filename "LetBinders.idr") (:start 3 13) (:end 3 14)) ((:decor :keyword)))))) 1)
diff --git a/tests/idris2/basic/basic002/Do.idr b/tests/idris2/basic/basic002/Do.idr
index 9da45c9f0..e3262f636 100644
--- a/tests/idris2/basic/basic002/Do.idr
+++ b/tests/idris2/basic/basic002/Do.idr
@@ -1,7 +1,7 @@
 data Maybe a = Nothing
              | Just a
 
-infixl 1 >>=
+private infixl 1 >>=
 
 (>>=) : Maybe a -> (a -> Maybe b) -> Maybe b
 (>>=) Nothing k = Nothing
diff --git a/tests/idris2/basic/basic003/Ambig2.idr b/tests/idris2/basic/basic003/Ambig2.idr
index 306805c23..b59ac7b5e 100644
--- a/tests/idris2/basic/basic003/Ambig2.idr
+++ b/tests/idris2/basic/basic003/Ambig2.idr
@@ -1,4 +1,4 @@
-infixr 5 ::
+private infixr 5 ::
 
 export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/basic/basic004/Stuff.idr b/tests/idris2/basic/basic004/Stuff.idr
index 73c10a4f1..87a3798c6 100644
--- a/tests/idris2/basic/basic004/Stuff.idr
+++ b/tests/idris2/basic/basic004/Stuff.idr
@@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/basic/basic006/Stuff.idr b/tests/idris2/basic/basic006/Stuff.idr
index c129ba5d2..c4d208de8 100644
--- a/tests/idris2/basic/basic006/Stuff.idr
+++ b/tests/idris2/basic/basic006/Stuff.idr
@@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/basic/basic007/Stuff.idr b/tests/idris2/basic/basic007/Stuff.idr
index c129ba5d2..c4d208de8 100644
--- a/tests/idris2/basic/basic007/Stuff.idr
+++ b/tests/idris2/basic/basic007/Stuff.idr
@@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/basic/basic009/Stuff.idr b/tests/idris2/basic/basic009/Stuff.idr
index 361f0a553..4421123bc 100644
--- a/tests/idris2/basic/basic009/Stuff.idr
+++ b/tests/idris2/basic/basic009/Stuff.idr
@@ -13,7 +13,7 @@ not False = True
 public export
 data Maybe a = Nothing | Just a
 
-infixl 4 &&
+export infixl 4 &&
 
 public export
 (&&) : Bool -> Lazy Bool -> Bool
@@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/basic/basic028/Do.idr b/tests/idris2/basic/basic028/Do.idr
index 9da45c9f0..e3262f636 100644
--- a/tests/idris2/basic/basic028/Do.idr
+++ b/tests/idris2/basic/basic028/Do.idr
@@ -1,7 +1,7 @@
 data Maybe a = Nothing
              | Just a
 
-infixl 1 >>=
+private infixl 1 >>=
 
 (>>=) : Maybe a -> (a -> Maybe b) -> Maybe b
 (>>=) Nothing k = Nothing
diff --git a/tests/idris2/basic/basic058/DataTypeOp.idr b/tests/idris2/basic/basic058/DataTypeOp.idr
index 36ac4e26f..1df6a2947 100644
--- a/tests/idris2/basic/basic058/DataTypeOp.idr
+++ b/tests/idris2/basic/basic058/DataTypeOp.idr
@@ -1,19 +1,19 @@
 --- Data declarations ---
 
-infix 0 =%=
+private infix 0 =%=
 
 public export
 data (=%=) : (a -> b) -> (a -> b) -> Type where
   ExtEq : {0 f, g : a -> b} -> ((x : a) -> f x = g x) -> f =%= g
 
-infix 0 %%
+private infix 0 %%
 
 public export
 data (%%) a b = Equs (a = b) (b = a)
 
 --- Records ---
 
-infix 0 =%%=
+private infix 0 =%%=
 
 public export
 record (=%%=) {a : Type} {b : Type} (f : a -> b) (g : a -> b) where
@@ -22,7 +22,7 @@ record (=%%=) {a : Type} {b : Type} (f : a -> b) (g : a -> b) where
 
 --- Interfaces ---
 
-infix 0 =%%%=
+private infix 0 =%%%=
 
 public export
 interface (=%%%=) (x : a) (y : a) (b : Type) (i : Type) where
diff --git a/tests/idris2/interface/interface001/IFace.idr b/tests/idris2/interface/interface001/IFace.idr
index 41e8f56ef..33d769c09 100644
--- a/tests/idris2/interface/interface001/IFace.idr
+++ b/tests/idris2/interface/interface001/IFace.idr
@@ -4,7 +4,7 @@ import Stuff
 
 %default partial
 
-infixl 5 ==, /=
+private infixl 5 ==, /=
 
 interface Eq b where
   (==) : b -> b -> Bool
diff --git a/tests/idris2/interface/interface001/IFace1.idr b/tests/idris2/interface/interface001/IFace1.idr
index 0a9d9ba30..1f9801fed 100644
--- a/tests/idris2/interface/interface001/IFace1.idr
+++ b/tests/idris2/interface/interface001/IFace1.idr
@@ -4,7 +4,7 @@ import Stuff
 
 %default partial
 
-infixl 5 ==, /=
+private infixl 5 ==, /=
 
 interface Eq b where
   (==) : b -> b -> Bool
diff --git a/tests/idris2/interface/interface001/Stuff.idr b/tests/idris2/interface/interface001/Stuff.idr
index 8e163324c..f63f76301 100644
--- a/tests/idris2/interface/interface001/Stuff.idr
+++ b/tests/idris2/interface/interface001/Stuff.idr
@@ -13,7 +13,7 @@ not False = True
 public export
 data Maybe a = Nothing | Just a
 
-infixl 4 &&
+export infixl 4 &&
 
 public export
 (&&) : Bool -> Bool -> Bool
@@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
@@ -52,7 +52,7 @@ public export
 data Equal : a -> b -> Type where
      Refl : {0 x : a} -> Equal x x
 
-infix 9 ===, ~=~
+export infix 9 ===, ~=~
 
 public export
 (===) : (x : a) -> (y : a) -> Type
diff --git a/tests/idris2/interface/interface002/Stuff.idr b/tests/idris2/interface/interface002/Stuff.idr
index 8bcc33117..e88a1aae5 100644
--- a/tests/idris2/interface/interface002/Stuff.idr
+++ b/tests/idris2/interface/interface002/Stuff.idr
@@ -36,7 +36,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/interface/interface006/Apply.idr b/tests/idris2/interface/interface006/Apply.idr
index 92407dfc2..8eca32865 100644
--- a/tests/idris2/interface/interface006/Apply.idr
+++ b/tests/idris2/interface/interface006/Apply.idr
@@ -2,7 +2,7 @@ module Apply
 
 -- These are not Biapplicatives.  Those are in Data.Biapplicative
 
-infixl 4 <<$>>, <<&>>, <<.>>, <<., .>>, <<..>>
+export infixl 4 <<$>>, <<&>>, <<.>>, <<., .>>, <<..>>
 
 ||| Primarily used to make the definitions of bilift2 and bilift3 pretty
 |||
diff --git a/tests/idris2/interface/interface006/Biapplicative.idr b/tests/idris2/interface/interface006/Biapplicative.idr
index 00c564309..22b14bde2 100644
--- a/tests/idris2/interface/interface006/Biapplicative.idr
+++ b/tests/idris2/interface/interface006/Biapplicative.idr
@@ -2,7 +2,7 @@ module Biapplicative
 
 import Apply
 
-infixl 4 <<*>>, <<*, *>>, <<**>>
+export infixl 4 <<*>>, <<*, *>>, <<**>>
 
 ||| Biapplicatives
 ||| @p the action of the Biapplicative on pairs of objects
diff --git a/tests/idris2/interface/interface006/Bimonad.idr b/tests/idris2/interface/interface006/Bimonad.idr
index d0eef33fc..b62f46888 100644
--- a/tests/idris2/interface/interface006/Bimonad.idr
+++ b/tests/idris2/interface/interface006/Bimonad.idr
@@ -2,7 +2,7 @@ module Bimonad
 
 import Biapplicative
 
-infixl 4 >>==
+export infixl 4 >>==
 
 ||| Bimonads
 ||| @p the action of the first Bifunctor component on pairs of objects
diff --git a/tests/idris2/interface/interface024/EH.idr b/tests/idris2/interface/interface024/EH.idr
index a03b2f94c..364f5e31e 100644
--- a/tests/idris2/interface/interface024/EH.idr
+++ b/tests/idris2/interface/interface024/EH.idr
@@ -1,8 +1,8 @@
 import Syntax.PreorderReasoning
 
 -------- some notation ----------
-infixr 6 .+.,:+:
-infixr 7 .*.,:*:
+private infixr 6 .+.,:+:
+private infixr 7 .*.,:*:
 
 interface Additive a where
   constructor MkAdditive
diff --git a/tests/idris2/linear/linear001/Stuff.idr b/tests/idris2/linear/linear001/Stuff.idr
index d0081e435..ffc56c203 100644
--- a/tests/idris2/linear/linear001/Stuff.idr
+++ b/tests/idris2/linear/linear001/Stuff.idr
@@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/linear/linear002/Stuff.idr b/tests/idris2/linear/linear002/Stuff.idr
index d0081e435..ffc56c203 100644
--- a/tests/idris2/linear/linear002/Stuff.idr
+++ b/tests/idris2/linear/linear002/Stuff.idr
@@ -43,7 +43,7 @@ plus : Nat -> Nat -> Nat
 plus Z y = y
 plus (S k) y = S (plus k y)
 
-infixr 5 ::
+export infixr 5 ::
 
 public export
 data List a = Nil | (::) a (List a)
diff --git a/tests/idris2/linear/linear012/linholes.idr b/tests/idris2/linear/linear012/linholes.idr
index f5bfdff78..0f5d6c979 100644
--- a/tests/idris2/linear/linear012/linholes.idr
+++ b/tests/idris2/linear/linear012/linholes.idr
@@ -1,4 +1,4 @@
-infixr 6 -*
+private infixr 6 -*
 (-*) : Type -> Type -> Type
 (-*) a b = (1 _ : a) -> b
 
diff --git a/tests/idris2/misc/docs004/List.idr b/tests/idris2/misc/docs004/List.idr
index aaac9b8bf..402f3b8c1 100644
--- a/tests/idris2/misc/docs004/List.idr
+++ b/tests/idris2/misc/docs004/List.idr
@@ -2,8 +2,8 @@ module List
 
 data List a = Nil | (::) a (List a)
 
-infixr 5 ::
-infixr 5 ++
+export infixr 5 ::
+export infixr 5 ++
 
 interface Monoid ty where
   ||| Users can hand-craft their own monoid implementations
diff --git a/tests/idris2/misc/import009/Test.idr b/tests/idris2/misc/import009/Test.idr
index 78aae7420..184d7600e 100644
--- a/tests/idris2/misc/import009/Test.idr
+++ b/tests/idris2/misc/import009/Test.idr
@@ -5,6 +5,7 @@ infixr 5 ~:>
 
 public export
 infixr 5 ~>
+export
 infixl 5 |>
 
 public export
diff --git a/tests/idris2/misc/lazy001/Lazy.idr b/tests/idris2/misc/lazy001/Lazy.idr
index 69bd065a6..7c34448a2 100644
--- a/tests/idris2/misc/lazy001/Lazy.idr
+++ b/tests/idris2/misc/lazy001/Lazy.idr
@@ -1,4 +1,4 @@
-infixr 5 ::
+private infixr 5 ::
 
 namespace List
     public export
diff --git a/tests/idris2/misc/namespace005/Lib1.idr b/tests/idris2/misc/namespace005/Lib1.idr
index f358c8153..b7ee29179 100644
--- a/tests/idris2/misc/namespace005/Lib1.idr
+++ b/tests/idris2/misc/namespace005/Lib1.idr
@@ -1,6 +1,6 @@
 module Lib1
 
-infixr 5 %%%
+export infixr 5 %%%
 
 export
 (%%%) : Nat -> Nat -> Nat
diff --git a/tests/idris2/misc/namespace005/Lib2.idr b/tests/idris2/misc/namespace005/Lib2.idr
index 8c8c8825e..0a0efa9d0 100644
--- a/tests/idris2/misc/namespace005/Lib2.idr
+++ b/tests/idris2/misc/namespace005/Lib2.idr
@@ -1,3 +1,3 @@
 module Lib2
 
-infixl 5 %%%
+export infixl 5 %%%
diff --git a/tests/idris2/misc/namespace005/LibPre1.idr b/tests/idris2/misc/namespace005/LibPre1.idr
index 9b8963c87..cdfedf0dc 100644
--- a/tests/idris2/misc/namespace005/LibPre1.idr
+++ b/tests/idris2/misc/namespace005/LibPre1.idr
@@ -1,6 +1,6 @@
 module LibPre1
 
-prefix 6 *!
+export prefix 6 *!
 
 export
 (*!) : Nat -> Nat
diff --git a/tests/idris2/misc/namespace005/LibPre2.idr b/tests/idris2/misc/namespace005/LibPre2.idr
index 7fff7c0fc..f045e6e12 100644
--- a/tests/idris2/misc/namespace005/LibPre2.idr
+++ b/tests/idris2/misc/namespace005/LibPre2.idr
@@ -1,3 +1,3 @@
 module LibPre2
 
-prefix 2 *!
+export prefix 2 *!
diff --git a/tests/idris2/misc/namespace005/Main3.idr b/tests/idris2/misc/namespace005/Main3.idr
index eae81a68b..a419e90cd 100644
--- a/tests/idris2/misc/namespace005/Main3.idr
+++ b/tests/idris2/misc/namespace005/Main3.idr
@@ -2,8 +2,8 @@ module Main3
 
 import Lib1
 
-prefix 4 %%%
-infixr 8 -
+private prefix 4 %%%
+private infixr 8 -
 
 (%%%) : Nat -> Nat
 (%%%) = S
diff --git a/tests/idris2/misc/namespace005/NonConflict1.idr b/tests/idris2/misc/namespace005/NonConflict1.idr
index d3c212bf3..6d5a64c8d 100644
--- a/tests/idris2/misc/namespace005/NonConflict1.idr
+++ b/tests/idris2/misc/namespace005/NonConflict1.idr
@@ -1,6 +1,6 @@
 module NonConflict1
 
-infixr 5 &&&
+export infixr 5 &&&
 
 export
 (&&&) : Nat -> Nat -> Nat
diff --git a/tests/idris2/misc/namespace005/NonConflict2.idr b/tests/idris2/misc/namespace005/NonConflict2.idr
index 4b767df4b..f73597be8 100644
--- a/tests/idris2/misc/namespace005/NonConflict2.idr
+++ b/tests/idris2/misc/namespace005/NonConflict2.idr
@@ -1,3 +1,3 @@
 module NonConflict2
 
-infixr 5 &&&
+export infixr 5 &&&
diff --git a/tests/idris2/misc/pretty001/Issue1328A.idr b/tests/idris2/misc/pretty001/Issue1328A.idr
index bb9a7cc96..9c15ca95b 100644
--- a/tests/idris2/misc/pretty001/Issue1328A.idr
+++ b/tests/idris2/misc/pretty001/Issue1328A.idr
@@ -1,7 +1,7 @@
 module Issue1328A
 %default total
 
-infix 4 `InCtx`
+private infix 4 `InCtx`
 data InCtx : (a, b : Type) -> Type where
 
 prop0 : a `InCtx` b
@@ -22,7 +22,7 @@ def1 m n = (`div` n) m
 def2 : (m, n : Integer) -> Integer
 def2 m n = (m `div`) n
 
-infix 4 |-
+private infix 4 |-
 data (|-) : (a, b : Type) -> Type where
 
 inProp0 : a |- b
diff --git a/tests/idris2/operators/operators001/Test.idr b/tests/idris2/operators/operators001/Test.idr
index c33218298..78f95861d 100644
--- a/tests/idris2/operators/operators001/Test.idr
+++ b/tests/idris2/operators/operators001/Test.idr
@@ -3,8 +3,8 @@ module Test
 
 import Data.Vect
 
-typebind infixr 0 =@
-infixr 0 -@
+private typebind infixr 0 =@
+private infixr 0 -@
 
 -- typebind infixr 1 =@@
 
@@ -39,7 +39,7 @@ map4 : (x : a) =@ (b -@ (y : List a) =@ List b)
 
 test3 : Test.map3 === Test.map4
 
-typebind infixr 0 *>
+private typebind infixr 0 *>
 
 -- (*>) : (ty : Type) -> (ty -> Type) -> Type
 -- (*>) = DPair
@@ -47,7 +47,7 @@ typebind infixr 0 *>
 -- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String
 -- testCompose = (1 ** 2 ** ["hello", "world", "!"])
 
-autobind infixr 0 `MyLet`
+private autobind infixr 0 `MyLet`
 
 MyLet : (val) -> (val -> rest) -> rest
 MyLet arg fn = fn arg
@@ -58,14 +58,14 @@ program = (n := 3) `MyLet` 2 + n
 program2 : Nat
 program2 = (n : Nat := 3) `MyLet` 2 + n
 
-typebind infixr 0 |>
+private typebind infixr 0 |>
 
 record Container where
   constructor (|>)
   shape : Type
   position : shape -> Type
 
-typebind infixr 0 @@
+private typebind infixr 0 @@
 
 record (@@) (x : Type) (y : x -> Type) where
   constructor PairUp
diff --git a/tests/idris2/operators/operators002/Error2.idr b/tests/idris2/operators/operators002/Error2.idr
index e3b6a420d..5d5e97893 100644
--- a/tests/idris2/operators/operators002/Error2.idr
+++ b/tests/idris2/operators/operators002/Error2.idr
@@ -1,5 +1,5 @@
 
-typebind infixr 0 =@
+private typebind infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
diff --git a/tests/idris2/operators/operators002/Errors.idr b/tests/idris2/operators/operators002/Errors.idr
index 4ee059bf5..89c69f796 100644
--- a/tests/idris2/operators/operators002/Errors.idr
+++ b/tests/idris2/operators/operators002/Errors.idr
@@ -1,5 +1,5 @@
 
-typebind infixr 0 =@
+private typebind infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
diff --git a/tests/idris2/operators/operators002/Errors2.idr b/tests/idris2/operators/operators002/Errors2.idr
index f7b6e7b22..f36ace64d 100644
--- a/tests/idris2/operators/operators002/Errors2.idr
+++ b/tests/idris2/operators/operators002/Errors2.idr
@@ -1,5 +1,5 @@
 
-autobind infixr 0 =@
+private autobind infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
diff --git a/tests/idris2/operators/operators002/Errors3.idr b/tests/idris2/operators/operators002/Errors3.idr
index 0e8994ec5..b9a7ec0cc 100644
--- a/tests/idris2/operators/operators002/Errors3.idr
+++ b/tests/idris2/operators/operators002/Errors3.idr
@@ -1,5 +1,5 @@
 
-typebind infixr 0 =@
+private typebind infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
diff --git a/tests/idris2/operators/operators002/Errors4.idr b/tests/idris2/operators/operators002/Errors4.idr
index d6a52f928..56e1786a8 100644
--- a/tests/idris2/operators/operators002/Errors4.idr
+++ b/tests/idris2/operators/operators002/Errors4.idr
@@ -1,5 +1,5 @@
 
-infixr 0 =@
+private infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
diff --git a/tests/idris2/operators/operators002/Errors5.idr b/tests/idris2/operators/operators002/Errors5.idr
index fd7225832..4e84a1e12 100644
--- a/tests/idris2/operators/operators002/Errors5.idr
+++ b/tests/idris2/operators/operators002/Errors5.idr
@@ -1,6 +1,6 @@
 
 
-infixr 0 =@
+private infixr 0 =@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
diff --git a/tests/idris2/operators/operators002/Lin.idr b/tests/idris2/operators/operators002/Lin.idr
new file mode 100644
index 000000000..830e53fd7
--- /dev/null
+++ b/tests/idris2/operators/operators002/Lin.idr
@@ -0,0 +1,4 @@
+module Lin
+
+export typebind infixr 0 =@
+
diff --git a/tests/idris2/operators/operators002/LinImport.idr b/tests/idris2/operators/operators002/LinImport.idr
new file mode 100644
index 000000000..c31930b5f
--- /dev/null
+++ b/tests/idris2/operators/operators002/LinImport.idr
@@ -0,0 +1,9 @@
+
+import Lin
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x := ty) =@ S x
+
diff --git a/tests/idris2/operators/operators002/Test.idr b/tests/idris2/operators/operators002/Test.idr
index b50c78f4c..901e7dda8 100644
--- a/tests/idris2/operators/operators002/Test.idr
+++ b/tests/idris2/operators/operators002/Test.idr
@@ -2,8 +2,8 @@
 
 import Data.Vect
 
-typebind infixr 0 =@
-infixr 0 -@
+private typebind infixr 0 =@
+private infixr 0 -@
 
 0 (=@) : (a : Type) -> (a -> Type) -> Type
 (=@) a f = (1 x : a) -> f x
@@ -18,7 +18,7 @@ data S : {ty : Type} -> (x : ty) -> Type where
   Mk4 : ty -@ (x : ty) =@ S x
   Chain : (x : ty =@ y : ty =@ S (x, y))
 
-typebind infixr 0 *>
+private typebind infixr 0 *>
 
 -- (*>) : (ty : Type) -> (ty -> Type) -> Type
 -- (*>) = DPair
@@ -26,7 +26,7 @@ typebind infixr 0 *>
 -- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String
 -- testCompose = (1 ** 2 ** ["hello", "world", "!"])
 
-autobind infixr 7 `MyLet`
+private autobind infixr 7 `MyLet`
 
 MyLet : (val) -> (val -> rest) -> rest
 MyLet arg fn = fn arg
diff --git a/tests/idris2/operators/operators002/expected b/tests/idris2/operators/operators002/expected
index 8451e1d0b..6da168498 100644
--- a/tests/idris2/operators/operators002/expected
+++ b/tests/idris2/operators/operators002/expected
@@ -12,8 +12,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using typebind syntax: '(x : ty) =@ S x'.
- - Change the fixity defined at Errors:2:10--2:21 to 'export autobind infixr 0 =@'.
- - Hide or remove the fixity at Errors:2:10--2:21 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Errors:2:18--2:29 to 'private autobind infixr 0 =@'.
+ - Hide or remove the fixity at Errors:2:18--2:29 and import a module that exports a compatible fixity.
 1/1: Building Errors2 (Errors2.idr)
 Error: Operator =@ is an automatically-binding (autobind) operator, but is used as a regular operator.
 
@@ -28,8 +28,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using autobind syntax: '(_ := a) =@ a'.
- - Change the fixity defined at Errors2:2:10--2:21 to 'export infixr 0 =@'.
- - Hide or remove the fixity at Errors2:2:10--2:21 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Errors2:2:18--2:29 to 'private infixr 0 =@'.
+ - Hide or remove the fixity at Errors2:2:18--2:29 and import a module that exports a compatible fixity.
 1/1: Building Errors3 (Errors3.idr)
 Error: Operator =@ is a type-binding (typebind) operator, but is used as a regular operator.
 
@@ -44,8 +44,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using typebind syntax: '(_ : a) =@ a'.
- - Change the fixity defined at Errors3:2:10--2:21 to 'export infixr 0 =@'.
- - Hide or remove the fixity at Errors3:2:10--2:21 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Errors3:2:18--2:29 to 'private infixr 0 =@'.
+ - Hide or remove the fixity at Errors3:2:18--2:29 and import a module that exports a compatible fixity.
 1/1: Building Errors4 (Errors4.idr)
 Error: Operator =@ is a regular operator, but is used as a type-binding (typebind) operator.
 
@@ -60,8 +60,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using regular syntax: 'ty =@ S x'.
- - Change the fixity defined at Errors4:2:1--2:12 to 'export typebind infixr 0 =@'.
- - Hide or remove the fixity at Errors4:2:1--2:12 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Errors4:2:9--2:20 to 'private typebind infixr 0 =@'.
+ - Hide or remove the fixity at Errors4:2:9--2:20 and import a module that exports a compatible fixity.
 1/1: Building Errors5 (Errors5.idr)
 Error: Operator =@ is a regular operator, but is used as an automatically-binding (autobind) operator.
 
@@ -76,5 +76,22 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using regular syntax: 'ty =@ S x'.
- - Change the fixity defined at Errors5:3:1--3:12 to 'export autobind infixr 0 =@'.
- - Hide or remove the fixity at Errors5:3:1--3:12 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Errors5:3:9--3:20 to 'private autobind infixr 0 =@'.
+ - Hide or remove the fixity at Errors5:3:9--3:20 and import a module that exports a compatible fixity.
+1/2: Building Lin (Lin.idr)
+2/2: Building LinImport (LinImport.idr)
+Error: Operator =@ is a type-binding (typebind) operator, but is used as an automatically-binding (autobind) operator.
+
+LinImport:8:19--8:21
+ 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type
+ 5 | (=@) a f = (1 x : a) -> f x
+ 6 | 
+ 7 | data S : {ty : Type} -> (x : ty) -> Type where
+ 8 |   MkS : (x := ty) =@ S x
+                       ^^
+Explanation: regular, typebind and autobind operators all use a slightly different syntax, typebind looks like this: '(name : type) =@ expr', autobind looks like this: '(name := expr) =@ expr'.
+
+Possible solutions:
+ - Write the expression using typebind syntax: '(x : ty) =@ S x'.
+ - Change the fixity defined at Lin:3:17--3:28 to 'export autobind infixr 0 =@'.
+ - Hide or remove the fixity at Lin:3:17--3:28 and import a module that exports a compatible fixity.
diff --git a/tests/idris2/operators/operators002/run b/tests/idris2/operators/operators002/run
index 13baec981..0edd4d47f 100755
--- a/tests/idris2/operators/operators002/run
+++ b/tests/idris2/operators/operators002/run
@@ -5,4 +5,5 @@ check Errors2.idr
 check Errors3.idr
 check Errors4.idr
 check Errors5.idr
+check LinImport.idr
 
diff --git a/tests/idris2/operators/operators004/Test.idr b/tests/idris2/operators/operators004/Test.idr
index 25093fc0e..bea8e1fb6 100644
--- a/tests/idris2/operators/operators004/Test.idr
+++ b/tests/idris2/operators/operators004/Test.idr
@@ -1,7 +1,7 @@
 
-infix 5 -:-
+private infix 5 -:-
 
-infix 5 :-:
+private infix 5 :-:
 
 (-:-) : a -> List a -> List a
 (-:-) = (::)
diff --git a/tests/idris2/operators/operators004/expected b/tests/idris2/operators/operators004/expected
index f976037ea..9a060b5ce 100644
--- a/tests/idris2/operators/operators004/expected
+++ b/tests/idris2/operators/operators004/expected
@@ -11,7 +11,7 @@ Test:13:8--13:22
 
 Possible solutions:
  - Add brackets around every use of -:-
- - Change the fixity of -:- at Test:2:1--2:12 to `infixl` or `infixr`
+ - Change the fixity of -:- at Test:2:9--2:20 to `infixl` or `infixr`
 Error: Operator :-: is non-associative
 
 Test:16:9--16:23
@@ -24,4 +24,4 @@ Test:16:9--16:23
 
 Possible solutions:
  - Add brackets around every use of :-:
- - Change the fixity of :-: at Test:4:1--4:12 to `infixl` or `infixr`
+ - Change the fixity of :-: at Test:4:9--4:20 to `infixl` or `infixr`
diff --git a/tests/idris2/operators/operators005/Test.idr b/tests/idris2/operators/operators005/Test.idr
index a96b27435..9e5a6a81a 100644
--- a/tests/idris2/operators/operators005/Test.idr
+++ b/tests/idris2/operators/operators005/Test.idr
@@ -1,8 +1,8 @@
 
 import Data.String
 
-typebind infixr 0 :-
-autobind infixr 0 `for`
+private typebind infixr 0 :-
+private autobind infixr 0 `for`
 
 record Container where
   constructor (:-)
diff --git a/tests/idris2/operators/operators006/Test.idr b/tests/idris2/operators/operators006/Test.idr
index b9aa1639c..d83d122e5 100644
--- a/tests/idris2/operators/operators006/Test.idr
+++ b/tests/idris2/operators/operators006/Test.idr
@@ -1,7 +1,7 @@
 
 import Data.Fin
 
-autobind infixr 0 `bind`
+private autobind infixr 0 `bind`
 
 bind : Monad m => m a -> (a -> m b) -> m b
 bind = (>>=)
diff --git a/tests/idris2/operators/operators007/Test.idr b/tests/idris2/operators/operators007/Test.idr
index b15090ce2..cc28d7cfa 100644
--- a/tests/idris2/operators/operators007/Test.idr
+++ b/tests/idris2/operators/operators007/Test.idr
@@ -1,7 +1,7 @@
 
 import Data.Fin
 
-autobind infixr 0 >>
+private autobind infixr 0 >>
 
 (>>) : Monad m => m a -> (a -> m b) -> m b
 (>>) = (>>=)
diff --git a/tests/idris2/operators/operators007/Test2.idr b/tests/idris2/operators/operators007/Test2.idr
index 021923a00..d16a843bd 100644
--- a/tests/idris2/operators/operators007/Test2.idr
+++ b/tests/idris2/operators/operators007/Test2.idr
@@ -1,8 +1,8 @@
 
 import Data.Fin
 
-autobind infixr 0 >>
-autobind infixr 0 >=
+private autobind infixr 0 >>
+private autobind infixr 0 >=
 
 (>>) : Monad m => m a -> (a -> m b) -> m b
 (>>) = (>>=)
diff --git a/tests/idris2/operators/operators007/expected b/tests/idris2/operators/operators007/expected
index 8644014d4..d93d1084e 100644
--- a/tests/idris2/operators/operators007/expected
+++ b/tests/idris2/operators/operators007/expected
@@ -12,8 +12,8 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using regular syntax: 'm >>= Just (x + y)'.
- - Change the fixity defined at Prelude.Ops:20:1--20:37 to 'export autobind infixl 1 >>='.
- - Hide or remove the fixity at Prelude.Ops:20:1--20:37 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Prelude.Ops:20:8--20:44 to 'export autobind infixl 1 >>='.
+ - Hide or remove the fixity at Prelude.Ops:20:8--20:44 and import a module that exports a compatible fixity.
  - Did you mean '>>' ?
 1/1: Building Test2 (Test2.idr)
 Error: Operator >>= is a regular operator, but is used as an automatically-binding (autobind) operator.
@@ -29,6 +29,6 @@ Explanation: regular, typebind and autobind operators all use a slightly differe
 
 Possible solutions:
  - Write the expression using regular syntax: 'm >>= Just (x + y)'.
- - Change the fixity defined at Prelude.Ops:20:1--20:37 to 'export autobind infixl 1 >>='.
- - Hide or remove the fixity at Prelude.Ops:20:1--20:37 and import a module that exports a compatible fixity.
+ - Change the fixity defined at Prelude.Ops:20:8--20:44 to 'export autobind infixl 1 >>='.
+ - Hide or remove the fixity at Prelude.Ops:20:8--20:44 and import a module that exports a compatible fixity.
  - Did you mean either of: '>=', '>>' ?
diff --git a/tests/idris2/operators/operators008/Test.idr b/tests/idris2/operators/operators008/Test.idr
index 328dfb3c2..8b7e1561c 100644
--- a/tests/idris2/operators/operators008/Test.idr
+++ b/tests/idris2/operators/operators008/Test.idr
@@ -4,7 +4,7 @@ import Test2
 
 %hide Test2.infixr.(@>)
 
-infixl 9 @>
+private infixl 9 @>
 
 (@>) : a -> b -> (a, b)
 (@>) = MkPair
diff --git a/tests/idris2/operators/operators009/Test.idr b/tests/idris2/operators/operators009/Test.idr
new file mode 100644
index 000000000..f4a1a92dc
--- /dev/null
+++ b/tests/idris2/operators/operators009/Test.idr
@@ -0,0 +1,4 @@
+
+infixr 0 =@
+export infixl 9 -:-
+
diff --git a/tests/idris2/operators/operators009/expected b/tests/idris2/operators/operators009/expected
new file mode 100644
index 000000000..a584bda3c
--- /dev/null
+++ b/tests/idris2/operators/operators009/expected
@@ -0,0 +1,11 @@
+1/1: Building Test (Test.idr)
+Warning: Fixity declaration 'infixr 0 =@' does not have an export modifier, and
+will become private by default in a future version.
+To expose it outside of its module, write 'export regular infixr 0 =@'. If you
+intend to keep it private, write 'private regular infixr 0 =@'.
+
+Test:2:1--2:12
+ 1 | 
+ 2 | infixr 0 =@
+     ^^^^^^^^^^^
+
diff --git a/tests/idris2/operators/operators009/run b/tests/idris2/operators/operators009/run
new file mode 100755
index 000000000..d35387bb3
--- /dev/null
+++ b/tests/idris2/operators/operators009/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Test.idr
diff --git a/tests/idris2/reflection/reflection016/Eta.idr b/tests/idris2/reflection/reflection016/Eta.idr
index ee191ceaf..21af530da 100644
--- a/tests/idris2/reflection/reflection016/Eta.idr
+++ b/tests/idris2/reflection/reflection016/Eta.idr
@@ -7,7 +7,7 @@ import Language.Reflection
 x : List String
 x = ["a", "b"]
 
-infixl 1 >==>
+private infixl 1 >==>
 
 -- From prelude:
 --(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
diff --git a/tests/idris2/reg/reg023/boom.idr b/tests/idris2/reg/reg023/boom.idr
index f740e38a0..c00ea99ab 100644
--- a/tests/idris2/reg/reg023/boom.idr
+++ b/tests/idris2/reg/reg023/boom.idr
@@ -2,7 +2,7 @@ import Data.Vect
 
 %default total
 
-infix 3 .<=.
+private infix 3 .<=.
 (.<=.) : Int -> Int -> Bool
 (.<=.) p q = case (p, q) of
   (0, _) => True
diff --git a/tests/idris2/reg/reg034/void.idr b/tests/idris2/reg/reg034/void.idr
index 11ee407d3..ba2a22e44 100644
--- a/tests/idris2/reg/reg034/void.idr
+++ b/tests/idris2/reg/reg034/void.idr
@@ -1,6 +1,6 @@
-infixl 0  ~~
-prefix 1  |~
-infix  1  ...
+private infixl 0  ~~
+private prefix 1  |~
+private infix  1  ...
 
 public export
 (...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z)
diff --git a/tests/idris2/warning/warning004/Lib1.idr b/tests/idris2/warning/warning004/Lib1.idr
index f358c8153..b7ee29179 100644
--- a/tests/idris2/warning/warning004/Lib1.idr
+++ b/tests/idris2/warning/warning004/Lib1.idr
@@ -1,6 +1,6 @@
 module Lib1
 
-infixr 5 %%%
+export infixr 5 %%%
 
 export
 (%%%) : Nat -> Nat -> Nat
diff --git a/tests/idris2/warning/warning004/Lib2.idr b/tests/idris2/warning/warning004/Lib2.idr
index 8c8c8825e..0a0efa9d0 100644
--- a/tests/idris2/warning/warning004/Lib2.idr
+++ b/tests/idris2/warning/warning004/Lib2.idr
@@ -1,3 +1,3 @@
 module Lib2
 
-infixl 5 %%%
+export infixl 5 %%%
diff --git a/tests/typedd-book/chapter06/DataStore.idr b/tests/typedd-book/chapter06/DataStore.idr
index 73406d2e6..b16fc3fbc 100644
--- a/tests/typedd-book/chapter06/DataStore.idr
+++ b/tests/typedd-book/chapter06/DataStore.idr
@@ -5,7 +5,7 @@ import Data.String
 import Data.Vect
 import System.REPL
 
-infixr 5 .+.
+private infixr 5 .+.
 
 data Schema = SString | SInt | (.+.) Schema Schema
 
diff --git a/tests/typedd-book/chapter06/DataStoreHoles.idr b/tests/typedd-book/chapter06/DataStoreHoles.idr
index 620760e9a..ed4cc0295 100644
--- a/tests/typedd-book/chapter06/DataStoreHoles.idr
+++ b/tests/typedd-book/chapter06/DataStoreHoles.idr
@@ -4,7 +4,7 @@ import Data.String
 import Data.Vect
 import System.REPL
 
-infixr 5 .+.
+private infixr 5 .+.
 
 data Schema = SString | SInt | (.+.) Schema Schema
 
diff --git a/tests/typedd-book/chapter10/DataStore.idr b/tests/typedd-book/chapter10/DataStore.idr
index ea10754ec..3ac4afda6 100644
--- a/tests/typedd-book/chapter10/DataStore.idr
+++ b/tests/typedd-book/chapter10/DataStore.idr
@@ -2,7 +2,7 @@ module DataStore
 
 import Data.Vect
 
-infixr 5 .+.
+export infixr 5 .+.
 
 public export
 data Schema = SString | SInt | (.+.) Schema Schema
diff --git a/tests/typedd-book/chapter12/DataStore.idr b/tests/typedd-book/chapter12/DataStore.idr
index a284db2df..e816c515f 100644
--- a/tests/typedd-book/chapter12/DataStore.idr
+++ b/tests/typedd-book/chapter12/DataStore.idr
@@ -2,7 +2,7 @@ module Main
 
 import Data.Vect
 
-infixr 5 .+.
+private infixr 5 .+.
 
 data Schema = SString | SInt | (.+.) Schema Schema