update libs with export modifier

idris-lang · Mar 15, 2024 · d6ac9a8 · d6ac9a8
1 parent 2bb8ce9
commit d6ac9a8
Show file tree

Hide file tree

Showing 47 changed files with 100 additions and 100 deletions.
diff --git 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
@@ -2,7 +2,7 @@ module Data.Contravariant
 
 %default total
 
-infixl 4 >$, >$<, >&<, $<
+export infixl 4 >$, >$<, >&<, $<
 
 ||| Contravariant functors
 public export

diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -30,8 +30,8 @@ plusAccZeroRightNeutral m =
   Refl
 
 
-infixl 4 -.
-infixr 4 .-
+export infixl 4 -.
+export infixr 4 .-
 
 namespace Left
 
@@ -158,7 +158,7 @@ namespace Right
 
 namespace Tree
 
-  infixl 4 ><
+  export infixl 4 ><
 
   mutual
     ||| A tree of dependent types
@@ -189,14 +189,14 @@ namespace Tree
          (transpL env1 ** snd (concat (delta (transpL env1))) env2)
     )
 
-infix 5 <++>
+export infix 5 <++>
 
 public export
 (<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
 [] <++> delta = delta ()
 (gamma -. sigma ) <++> delta = gamma <++> (\ env => sigma env .- \ v => delta (env ** v))
 
-infix 5 >++<
+export infix 5 >++<
 
 (>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
          Left.Telescope (plusAcc m n)

diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr
@@ -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
@@ -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
@@ -122,7 +122,7 @@ export
 fill : Int -> Doc ann -> Doc ann
 fill n doc = width doc (\w => spaces $ n - w)
 
-infixr 6 <++>
+export infixr 6 <++>
 ||| Concatenates two documents with a space in between.
 export
 (<++>) : Doc ann -> Doc ann -> Doc ann

diff --git a/libs/linear/Data/Linear/Interface.idr b/libs/linear/Data/Linear/Interface.idr
@@ -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
@@ -2,7 +2,7 @@ module Data.Linear.Notation
 
 %default total
 
-infixr 0 -@
+export infixr 0 -@
 ||| Infix notation for linear implication
 public export
 (-@) : Type -> Type -> Type

diff --git a/libs/papers/Data/Description/Regular.idr b/libs/papers/Data/Description/Regular.idr
@@ -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
@@ -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
@@ -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
@@ -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