[ agda#6055 ] Updated std-lib commit (in the release-v1.7.2 branch).

JobPetrovcic · Apr 5, 2024 · 8f98e77 · 8f98e77
1 parent c8ac2fd
commit 8f98e77
Show file tree

Hide file tree

Showing 13 changed files with 668 additions and 51 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1,7 +1,3 @@
-[submodule "std-lib"]
-	path = std-lib
-	url = https://github.com/agda/agda-stdlib
-	branch = master
 [submodule "cubical"]
 	path = cubical
 	url = https://github.com/agda/cubical
diff --git a/benchmark/monad/Monad.agda b/benchmark/monad/Monad.agda
@@ -50,10 +50,10 @@ open STOProps (record { Carrier = _ ; _≈_ = _; _<_ = _
                       ; isStrictTotalOrder = posOrdered })
 
 import IndexedMap as Map -- renaming (Map to MemoTable)
-open import Effect.Monad
-open import Effect.Monad.State
+open import Category.Monad
+open import Category.Monad.State
 import Data.List as List; open List using (List)
-open import Data.Unit
+open import Data.Unit hiding (poset; _≤_)
 open import Function
 open import Data.Maybe
 open import Data.Product.Relation.Binary.Lex.Strict

diff --git a/benchmark/monad/MonadPostulates.agda b/benchmark/monad/MonadPostulates.agda
@@ -53,10 +53,10 @@ open STOProps (record { Carrier = _ ; _≈_ = _; _<_ = _
                       ; isStrictTotalOrder = posOrdered })
 
 import IndexedMap as Map -- renaming (Map to MemoTable)
-open import Effect.Monad
-open import Effect.Monad.State
+open import Category.Monad
+open import Category.Monad.State
 import Data.List as List; open List using (List)
-open import Data.Unit
+open import Data.Unit hiding (poset; _≤_)
 open import Function
 open import Data.Maybe
 open import Data.Product.Relation.Binary.Lex.Strict