[Import] Induction...Level (#2642)

* [Import] ...

* [Import] ...

* Update src/Induction/WellFounded.agda

* Update src/Induction/WellFounded.agda

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: jmougeot

src/IO/Base.agda

@@ -8,15 +8,16 @@
 
 module IO.Base where
 
-open import Level
-open import Codata.Musical.Notation
-open import Data.Bool.Base using (Bool; true; false; not)
 open import Agda.Builtin.Maybe using (Maybe; nothing; just)
+open import Codata.Musical.Notation using (♭; ♯_; ∞)
+open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-import Agda.Builtin.Unit as Unit0
-open import Data.Unit.Polymorphic.Base
+open import Data.Unit.Polymorphic.Base using (⊤)
 open import Function.Base using (_∘′_; const; flip)
-import IO.Primitive.Core as Prim
+open import Level using (Level; Lift; lower; 0ℓ; suc)
+
+import Agda.Builtin.Unit as Unit0 using (⊤)
+import IO.Primitive.Core as Prim using (IO; pure; _>>=_; _>>_)
 
 private
   variable

src/IO/Effectful.agda

@@ -8,10 +8,10 @@
 
 module IO.Effectful where
 
-open import Level
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
+open import Level using (Level; _⊔_)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad)
 
 open import IO.Base
 

src/IO/Finite.agda

@@ -8,13 +8,14 @@
 
 module IO.Finite where
 
-open import Data.Unit.Polymorphic.Base
-open import Agda.Builtin.String
-import Data.Unit.Base as Unit0
-open import IO.Base
-import IO.Primitive.Core as Prim
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import Agda.Builtin.String using (String)
+import Data.Unit.Base as Unit0 using (⊤)
+open import IO.Base as Base using (IO; lift; lift′)
+import IO.Primitive.Core as Prim using (IO; _>>=_; _>>_)
 import IO.Primitive.Finite as Prim
-open import Level
+  using (getLine; readFile; writeFile; appendFile; putStr; putStrLn)
+open import Level using (Level; Lift; 0ℓ; suc)
 
 private
   variable

src/IO/Infinite.agda

@@ -8,14 +8,15 @@
 
 module IO.Infinite where
 
-open import Codata.Musical.Costring
-open import Agda.Builtin.String
-open import Data.Unit.Polymorphic.Base
-import Data.Unit.Base as Unit0
-open import IO.Base
-import IO.Primitive.Core as Prim
+open import Codata.Musical.Costring using (Costring)
+open import Agda.Builtin.String using (String)
+open import Data.Unit.Polymorphic.Base using (⊤)
+import Data.Unit.Base as Unit0 using (⊤)
+open import IO.Base as Base using (IO; lift; lift′)
+import IO.Primitive.Core as Prim using (IO; _>>=_; _>>_)
 import IO.Primitive.Infinite as Prim
-open import Level
+  using (getContents; writeFile; appendFile; putStr; putStrLn)
+open import Level using (Level; Lift; 0ℓ; suc)
 
 private
   variable

src/IO/Instances.agda

@@ -8,11 +8,11 @@
 
 module IO.Instances where
 
-open import IO.Base
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import IO.Effectful
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad)
+open import IO.Base using (IO)
+open import IO.Effectful using (functor; applicative; monad)
 
 instance
   ioFunctor = functor

src/IO/Primitive/Finite.agda

@@ -12,8 +12,8 @@ module IO.Primitive.Finite where
 -- NOTE: the contents of this module should be accessed via `IO` or
 -- `IO.Finite`.
 
-open import Agda.Builtin.IO
-open import Agda.Builtin.String
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.String using (String)
 open import Agda.Builtin.Unit using () renaming (⊤ to Unit)
 
 ------------------------------------------------------------------------

src/IO/Primitive/Infinite.agda

@@ -12,8 +12,8 @@ module IO.Primitive.Infinite where
 -- NOTE: the contents of this module should be accessed via `IO` or
 -- `IO.Infinite`.
 
-open import Codata.Musical.Costring
-open import Agda.Builtin.String
+open import Codata.Musical.Costring using (Costring)
+open import Agda.Builtin.String using (String)
 open import Agda.Builtin.Unit renaming (⊤ to Unit)
 
 ------------------------------------------------------------------------

src/Induction/Lexicographic.agda

@@ -9,8 +9,8 @@
 module Induction.Lexicographic where
 
 open import Data.Product.Base using (Σ; _,_; _×_)
-open import Induction
-open import Level
+open import Induction using (RecStruct; RecursorBuilder; build)
+open import Level using (Level; _⊔_)
 
 -- The structure of lexicographic induction.
 

src/Induction/WellFounded.agda

@@ -11,14 +11,17 @@ module Induction.WellFounded where
 open import Data.Product.Base using (Σ; _,_; proj₁; proj₂)
 open import Function.Base using (_∘_; flip; _on_)
 open import Induction
+  using (RecStruct; RecursorBuilder; Recursor; build
+        ; SubsetRecursorBuilder; SubsetRecursor; subsetBuild)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions
-  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_;
-    _Respectsʳ_; _Respects_)
+  using (Symmetric; Asymmetric; Irreflexive
+        ; _Respects₂_; _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Unary
+  using (Pred; _⊆′_; _⊆_; _⇒_; Universal; IUniversal; Stable; Empty)
 open import Relation.Nullary.Negation.Core using (¬_)
 
 private

src/Level/Literals.agda

@@ -9,8 +9,8 @@
 module Level.Literals where
 
 open import Agda.Builtin.Nat renaming (Nat to ℕ)
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.Unit
+open import Agda.Builtin.FromNat using (Number)
+open import Agda.Builtin.Unit using (⊤)
 open import Level using (Level; 0ℓ)
 
 -- Increase a Level by a number of sucs.