knock-ons

Author: jamesmckinna

src/Codata/Sized/Colist/Properties.agda

@@ -22,7 +22,7 @@ open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
-import Data.List.Scans as Scans
+import Data.List.Scans.Base as Scans
 open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 import Data.Maybe.Properties as Maybe

src/Tactic/RingSolver/Core/NatSet.agda

@@ -38,7 +38,7 @@ module Tactic.RingSolver.Core.NatSet where
 
 open import Data.Nat.Base   as ℕ     using (ℕ; suc; zero)
 open import Data.List.Base  as List  using (List; _∷_; [])
-open import Data.List.Scans as Scans using (scanl)
+open import Data.List.Scans.Base as Scans using (scanl)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Bool.Base  as Bool  using (Bool)
 open import Function.Base            using (const; _∘_)