From 1d64ac0f3620639fed2ebb92f567e0a8c36012b0 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 8 Jul 2025 20:48:33 -0500
Subject: [PATCH 01/15] Update polymorphic runParser for stdlib 2.0

---
 src/Text/Parser/Polymorphic.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Text/Parser/Polymorphic.agda b/src/Text/Parser/Polymorphic.agda
index 885de44..d4a4e86 100644
--- a/src/Text/Parser/Polymorphic.agda
+++ b/src/Text/Parser/Polymorphic.agda
@@ -59,6 +59,7 @@ open import Data.Nat.Base using (_≡ᵇ_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (_,_)
 open import Data.String as String using (String)
+open import Effect.Monad.State.Transformer using (runStateT)
 open import Function.Base using (case_of_)
 
 import Text.Parser.Monad.Result as Result
@@ -68,8 +69,8 @@ runParser : {A : Set≤ l} → ∀[ Parser A ] → String → Position ⊎ theSe
 runParser p str =
   let init  = lift (start , [])
       input = lift (String.toVec str)
-  in case Result.toSum (Parser.runParser p (ℕₚ.n≤1+n _) input init) of λ where
-        (inj₂ (res , p)) → let open Success in
+  in case Result.toSum (runStateT (Parser.runParser p (ℕₚ.n≤1+n _) input) init) of λ where
+        (inj₂ (p , res)) → let open Success in
                            if size res ≡ᵇ 0
                            then inj₂ (lower (value res))
                            else inj₁ (proj₁ (lower p))

From 2fa8bc5fd62e641751c355c87edb4e94285802bd Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 9 Jul 2025 17:50:51 -0500
Subject: [PATCH 02/15] Update stdlib version in README

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 261c4a7..1687a70 100644
--- a/README.md
+++ b/README.md
@@ -12,7 +12,7 @@ The motivation and design decisions behind agdarsec are detailed in:
 To typecheck and compile this project you will need:
 
 * Agda version 2.6.2
-* Agda's standard library (version 1.7)
+* Agda's standard library (version 2.0)
 
 ## Ports
 

From 1ab92a19a73624e7286536b936bdabc1d0adb664 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 16 Jul 2025 12:05:27 +0100
Subject: [PATCH 03/15] [ ci ] bump checkout to v4

---
 .github/workflows/ci-ubuntu.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 2bb4c5e..15b033a 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -134,7 +134,7 @@ jobs:
 
       # By default github actions do not pull the repo
       - name: Checkout agdarsec
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
 
       # Generate a fresh Everything.agda & index.agda and start building!
       - name: Test agdarsec

From cecf229354424c71a6deda8a2589e97aa0e5e652 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 16 Jul 2025 12:07:31 +0100
Subject: [PATCH 04/15] [ ci ] add import of Polymorphic version for testing

---
 index.agda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/index.agda b/index.agda
index 5a2db14..f75c321 100644
--- a/index.agda
+++ b/index.agda
@@ -5,6 +5,10 @@ module index where
 -- The core design decisions behind agdarsec are detailed in
 -- https://gallais.github.io/pdf/agdarsec18.pdf
 
+-- The most general version of the library is in
+
+import Text.Parser.Polymorphic
+
 -- We have a simplified frontend with ready made default choices:
 
 import Text.Parser

From 51dc110a7b2bc2be2f6f33335b43c94be5116da1 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 16 Jul 2025 12:08:22 +0100
Subject: [PATCH 05/15] [ ci ] bump cache to v4 too

---
 .github/workflows/ci-ubuntu.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 15b033a..277a65f 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -83,7 +83,7 @@ jobs:
       # i.e. if we change either the version of Agda, ghc, or cabal that we want
       # to use for the build.
       - name: Cache cabal packages
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         id: cache-cabal
         with:
           path: |

From 10a399f578b236c2d88e4423ded36e7c000cee1a Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Wed, 16 Jul 2025 13:26:47 +0100
Subject: [PATCH 06/15] [ ci ] bump dependency versions

---
 .github/workflows/ci-ubuntu.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 277a65f..e4dc19a 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -45,8 +45,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_COMMIT: tags/v2.6.2
-  STDLIB_VERSION: 1.7
+  AGDA_COMMIT: tags/v2.6.4.3
+  STDLIB_VERSION: 2.0
 
   GHC_VERSION: 8.6.5
   CABAL_VERSION: 3.2.0.0

From 1289a5ce072185abaca413636d2d790b9a19fc11 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 29 Jul 2025 16:15:19 +0100
Subject: [PATCH 07/15] [ ci ] full version number

---
 .github/workflows/ci-ubuntu.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index e4dc19a..04cf15c 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -46,7 +46,7 @@ on:
 
 env:
   AGDA_COMMIT: tags/v2.6.4.3
-  STDLIB_VERSION: 2.0
+  STDLIB_VERSION: '2.0'
 
   GHC_VERSION: 8.6.5
   CABAL_VERSION: 3.2.0.0

From 025f888c833ecbbb89c2fbdb10837cbc8077adaf Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 29 Jul 2025 16:39:47 +0100
Subject: [PATCH 08/15] [ fix ] error

---
 examples/Expr.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/examples/Expr.agda b/examples/Expr.agda
index 1b82e7f..8e6e6e9 100644
--- a/examples/Expr.agda
+++ b/examples/Expr.agda
@@ -1,6 +1,8 @@
 -- Example taken from parsec's documentation
 -- https://hackage.haskell.org/package/parsec-3.1.11/docs/Text-Parsec-Combinator.html#v:chainl1
 
+{-# OPTIONS --guardedness #-}
+
 module Expr where
 
 

From 97fe0c8d3c995110be74e2ce558ec5fa4ba7a92d Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 29 Jul 2025 16:40:25 +0100
Subject: [PATCH 09/15] [ ci ] temporarily comment bits off

Should get us the caching behaviour & speed up the
next builds
---
 .github/workflows/ci-ubuntu.yml | 74 ++++++++++++++++-----------------
 1 file changed, 37 insertions(+), 37 deletions(-)

diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 04cf15c..7a9acf5 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -118,40 +118,40 @@ jobs:
           ${{ env.CABAL_INSTALL }}
           cd ..
 
-      - name: Install stdlib
-        run: |
-          mkdir -p $HOME/.agda
-          cd $HOME/.agda
-          wget https://github.com/agda/agda-stdlib/archive/v${{ env.STDLIB_VERSION }}.tar.gz
-          tar -xzvf v${{ env.STDLIB_VERSION }}.tar.gz
-          mv agda-stdlib-${{ env.STDLIB_VERSION }} agda-stdlib
-          echo "~/.agda/agda-stdlib/standard-library.agda-lib" > libraries
-          cd -
-
-########################################################################
-## TESTING AND DEPLOYMENT
-########################################################################
-
-      # By default github actions do not pull the repo
-      - name: Checkout agdarsec
-        uses: actions/checkout@v4
-
-      # Generate a fresh Everything.agda & index.agda and start building!
-      - name: Test agdarsec
-        run: |
-          ${{ env.AGDA }} -iexamples index.agda
-
-      # Note that if you want to deploy html for different versions like the
-      # standard library does, you will need to be a bit more subtle in this
-      # step.
-      - name: Generate HTML
-        run: |
-          ${{ env.AGDA }} -iexamples --html --html-dir html index.agda
-
-      - name: Deploy HTML
-        uses: JamesIves/github-pages-deploy-action@4.1.3
-        if: ${{ success() && env.AGDA_DEPLOY }}
-
-        with:
-          branch: gh-pages
-          folder: html
+#       - name: Install stdlib
+#         run: |
+#           mkdir -p $HOME/.agda
+#           cd $HOME/.agda
+#           wget https://github.com/agda/agda-stdlib/archive/v${{ env.STDLIB_VERSION }}.tar.gz
+#           tar -xzvf v${{ env.STDLIB_VERSION }}.tar.gz
+#           mv agda-stdlib-${{ env.STDLIB_VERSION }} agda-stdlib
+#           echo "~/.agda/agda-stdlib/standard-library.agda-lib" > libraries
+#           cd -
+
+# ########################################################################
+# ## TESTING AND DEPLOYMENT
+# ########################################################################
+
+#       # By default github actions do not pull the repo
+#       - name: Checkout agdarsec
+#         uses: actions/checkout@v4
+
+#       # Generate a fresh Everything.agda & index.agda and start building!
+#       - name: Test agdarsec
+#         run: |
+#           ${{ env.AGDA }} -iexamples index.agda
+
+#       # Note that if you want to deploy html for different versions like the
+#       # standard library does, you will need to be a bit more subtle in this
+#       # step.
+#       - name: Generate HTML
+#         run: |
+#           ${{ env.AGDA }} -iexamples --html --html-dir html index.agda
+
+#       - name: Deploy HTML
+#         uses: JamesIves/github-pages-deploy-action@4.1.3
+#         if: ${{ success() && env.AGDA_DEPLOY }}
+
+#         with:
+#           branch: gh-pages
+#           folder: html

From 0bc6e8752419ec142644359cb8741c33aa8dd9d8 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 29 Jul 2025 17:14:11 +0100
Subject: [PATCH 10/15] [ ci ] full build

---
 .github/workflows/ci-ubuntu.yml | 74 ++++++++++++++++-----------------
 1 file changed, 37 insertions(+), 37 deletions(-)

diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 7a9acf5..04cf15c 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -118,40 +118,40 @@ jobs:
           ${{ env.CABAL_INSTALL }}
           cd ..
 
-#       - name: Install stdlib
-#         run: |
-#           mkdir -p $HOME/.agda
-#           cd $HOME/.agda
-#           wget https://github.com/agda/agda-stdlib/archive/v${{ env.STDLIB_VERSION }}.tar.gz
-#           tar -xzvf v${{ env.STDLIB_VERSION }}.tar.gz
-#           mv agda-stdlib-${{ env.STDLIB_VERSION }} agda-stdlib
-#           echo "~/.agda/agda-stdlib/standard-library.agda-lib" > libraries
-#           cd -
-
-# ########################################################################
-# ## TESTING AND DEPLOYMENT
-# ########################################################################
-
-#       # By default github actions do not pull the repo
-#       - name: Checkout agdarsec
-#         uses: actions/checkout@v4
-
-#       # Generate a fresh Everything.agda & index.agda and start building!
-#       - name: Test agdarsec
-#         run: |
-#           ${{ env.AGDA }} -iexamples index.agda
-
-#       # Note that if you want to deploy html for different versions like the
-#       # standard library does, you will need to be a bit more subtle in this
-#       # step.
-#       - name: Generate HTML
-#         run: |
-#           ${{ env.AGDA }} -iexamples --html --html-dir html index.agda
-
-#       - name: Deploy HTML
-#         uses: JamesIves/github-pages-deploy-action@4.1.3
-#         if: ${{ success() && env.AGDA_DEPLOY }}
-
-#         with:
-#           branch: gh-pages
-#           folder: html
+      - name: Install stdlib
+        run: |
+          mkdir -p $HOME/.agda
+          cd $HOME/.agda
+          wget https://github.com/agda/agda-stdlib/archive/v${{ env.STDLIB_VERSION }}.tar.gz
+          tar -xzvf v${{ env.STDLIB_VERSION }}.tar.gz
+          mv agda-stdlib-${{ env.STDLIB_VERSION }} agda-stdlib
+          echo "~/.agda/agda-stdlib/standard-library.agda-lib" > libraries
+          cd -
+
+########################################################################
+## TESTING AND DEPLOYMENT
+########################################################################
+
+      # By default github actions do not pull the repo
+      - name: Checkout agdarsec
+        uses: actions/checkout@v4
+
+      # Generate a fresh Everything.agda & index.agda and start building!
+      - name: Test agdarsec
+        run: |
+          ${{ env.AGDA }} -iexamples index.agda
+
+      # Note that if you want to deploy html for different versions like the
+      # standard library does, you will need to be a bit more subtle in this
+      # step.
+      - name: Generate HTML
+        run: |
+          ${{ env.AGDA }} -iexamples --html --html-dir html index.agda
+
+      - name: Deploy HTML
+        uses: JamesIves/github-pages-deploy-action@4.1.3
+        if: ${{ success() && env.AGDA_DEPLOY }}
+
+        with:
+          branch: gh-pages
+          folder: html

From 2391bd1b86e23b1627da02f7efd6f3cba1becbe1 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 1 Aug 2025 15:59:44 +0100
Subject: [PATCH 11/15] [ fix ] add missing --guardedness OPTIONS

---
 examples/Base.agda        | 2 ++
 examples/Identifier.agda  | 2 ++
 examples/Large.agda       | 2 ++
 examples/NList.agda       | 2 ++
 examples/Parentheses.agda | 2 ++
 examples/RegExp.agda      | 2 ++
 examples/SExp.agda        | 2 ++
 examples/STLC.agda        | 2 ++
 8 files changed, 16 insertions(+)

diff --git a/examples/Base.agda b/examples/Base.agda
index 69fc61a..6397725 100644
--- a/examples/Base.agda
+++ b/examples/Base.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 open import Level using (Level)
 
 module Base (l : Level) where
diff --git a/examples/Identifier.agda b/examples/Identifier.agda
index d6f5849..aa43de1 100644
--- a/examples/Identifier.agda
+++ b/examples/Identifier.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module Identifier where
 
 import Level
diff --git a/examples/Large.agda b/examples/Large.agda
index 0c5dee0..1e1a947 100644
--- a/examples/Large.agda
+++ b/examples/Large.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module Large where
 
 import Level
diff --git a/examples/NList.agda b/examples/NList.agda
index 826f671..23d82cb 100644
--- a/examples/NList.agda
+++ b/examples/NList.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 -- Challenge taken from stackoverflow:
 -- http://stackoverflow.com/questions/12380239/agda-parsing-nested-lists
 
diff --git a/examples/Parentheses.agda b/examples/Parentheses.agda
index 6f80c9a..a3a5c07 100644
--- a/examples/Parentheses.agda
+++ b/examples/Parentheses.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module Parentheses where
 
 import Level
diff --git a/examples/RegExp.agda b/examples/RegExp.agda
index a0d7925..544ef1c 100644
--- a/examples/RegExp.agda
+++ b/examples/RegExp.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module RegExp where
 
 import Level
diff --git a/examples/SExp.agda b/examples/SExp.agda
index 83b9d03..e20afb1 100644
--- a/examples/SExp.agda
+++ b/examples/SExp.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module SExp where
 
 open import Level using (0ℓ)
diff --git a/examples/STLC.agda b/examples/STLC.agda
index 7f26d90..db11684 100644
--- a/examples/STLC.agda
+++ b/examples/STLC.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 module STLC where
 
 open import Level.Bounded using ([_])

From 72ddb00f97782079ff528cc743004a000f577aae Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 1 Aug 2025 16:34:06 +0100
Subject: [PATCH 12/15] [ fix ] 'Categorical' has been deprecated

---
 examples/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/Base.agda b/examples/Base.agda
index 6397725..e1a1c29 100644
--- a/examples/Base.agda
+++ b/examples/Base.agda
@@ -13,14 +13,14 @@ import Data.Empty as Empty
 open import Data.Product as Product using (_,_; proj₁)
 
 open import Data.List.Base as List using ([]; _∷_)
-open import Data.List.Categorical as List
+open import Data.List.Effectful as List
 open import Data.List.Sized.Interface
 
 open import Data.String as String
 open import Data.Vec as Vec using ()
 open import Data.Bool
 open import Data.Maybe as Maybe using (nothing; just; maybe′)
-open import Data.Maybe.Categorical as MaybeCat
+open import Data.Maybe.Effectful as MaybeCat
 open import Data.Sum
 open import Function
 open import Category.Monad

From 5df66d8f690a27a266a301c1510f14aeec603f7c Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Fri, 1 Aug 2025 17:03:10 +0100
Subject: [PATCH 13/15] [ fix ] Category. has moved to Effect.

---
 examples/Base.agda | 4 ++--
 examples/SExp.agda | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/examples/Base.agda b/examples/Base.agda
index e1a1c29..f3c6bb7 100644
--- a/examples/Base.agda
+++ b/examples/Base.agda
@@ -23,8 +23,8 @@ open import Data.Maybe as Maybe using (nothing; just; maybe′)
 open import Data.Maybe.Effectful as MaybeCat
 open import Data.Sum
 open import Function
-open import Category.Monad
-open import Category.Monad.State
+open import Effect.Monad
+open import Effect.Monad.State
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
diff --git a/examples/SExp.agda b/examples/SExp.agda
index e20afb1..3e883c5 100644
--- a/examples/SExp.agda
+++ b/examples/SExp.agda
@@ -11,7 +11,7 @@ data SExp : Set where
   Atom : String → SExp
   Pair : SExp → SExp → SExp
 
-open import Category.Monad
+open import Effect.Monad
 open import Data.List.Sized.Interface
 open import Data.List.NonEmpty as List⁺ using (List⁺)
 open import Data.Maybe

From af6e2f76a37cfec920b2a870a87e128bc32f2764 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 5 Aug 2025 16:39:23 +0100
Subject: [PATCH 14/15] [ fix ] all the remaining bits

Gave up and dealt with it offline given there were many subtle
things (e.g. introduced by the new definition of StateT).
---
 Makefile             | 3 ++-
 examples/Base.agda   | 7 ++++---
 examples/Matrix.agda | 8 +++++---
 examples/STLC.agda   | 5 ++++-
 examples/Vec.agda    | 8 +++++---
 5 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/Makefile b/Makefile
index 20eaee0..86cae9c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,13 @@
 AGDA_EXEC?=agda
 .PHONY: test Everything.agda clean
 
-OTHEROPTS = --auto-inline -Werror
+OTHEROPTS = -Werror
 
 RTSARGS = +RTS -M6G -A128M -RTS ${OTHEROPTS}
 
 test: Everything.agda
 	${AGDA_EXEC} ${RTSARGS} -i. Everything.agda
+	${AGDA_EXEC} ${RTSARGS} -i. -i src/ -iexamples index.agda
 
 html: Everything.agda
 	${AGDA_EXEC} ${RTSARGS} --html -i. Everything.agda
diff --git a/examples/Base.agda b/examples/Base.agda
index f3c6bb7..491d700 100644
--- a/examples/Base.agda
+++ b/examples/Base.agda
@@ -10,7 +10,7 @@ import Data.Nat as Nat
 open import Data.Nat.Properties
 open import Data.Char.Base as Char using (Char)
 import Data.Empty as Empty
-open import Data.Product as Product using (_,_; proj₁)
+open import Data.Product as Product using (_,_; proj₂)
 
 open import Data.List.Base as List using ([]; _∷_)
 open import Data.List.Effectful as List
@@ -24,7 +24,7 @@ open import Data.Maybe.Effectful as MaybeCat
 open import Data.Sum
 open import Function
 open import Effect.Monad
-open import Effect.Monad.State
+open import Effect.Monad.State.Transformer as StateT using (StateT)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
@@ -83,9 +83,10 @@ instance
 
   runStateT : ∀ {M A} {{𝕄 : RawMonadRun M}} → RawMonadRun (StateT (Lift ([ Position ] × List A)) M)
   runStateT {{𝕄}} .RawMonadRun.runM =
-    List.map proj₁
+    List.map proj₂
     ∘′ runM 𝕄
     ∘′ (_$ lift (start , []))
+    ∘′ StateT.runStateT
 
   monadMaybe : RawMonad {l} Maybe.Maybe
   monadMaybe = MaybeCat.monad
diff --git a/examples/Matrix.agda b/examples/Matrix.agda
index 1dc90ef..db7d3b6 100644
--- a/examples/Matrix.agda
+++ b/examples/Matrix.agda
@@ -1,8 +1,10 @@
+{-# OPTIONS --guardedness #-}
+
 module Matrix where
 
 open import Data.Maybe.Base as Maybe
-open import Data.Nat.Base
-open import Data.Product as Product
+open import Data.Nat.Base hiding (_!)
+open import Data.Product.Base as Product
 open import Data.Sum.Base
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Function.Base
@@ -26,7 +28,7 @@ indices = f <$> (decimalℕ <& box space <&> box decimalℕ) where
   f (suc m , suc n) = inj₂ (suc m , suc n , _)
 
 matrix : ∀[ Parser (Σ[ m ∈ ℕ ] Σ[ n ∈ ℕ ] Matrix ℕ m n) ]
-matrix = <[ ((λ (m , n , p) → [ (λ _ → 0 , n , []) , (λ _ → m , 0 , Vec.replicate []) ] p))
+matrix = <[ ((λ (m , n , p) → [ (λ _ → 0 , n , []) , (λ _ → m , 0 , Vec.replicate _ []) ] p))
           , (λ (m , n , p , q) → box $ (m ,_) ∘ (n ,_) <$> replicate m {{p}} (replicate n {{q}} (space &> box decimalℕ)))
           ]> indices
 
diff --git a/examples/STLC.agda b/examples/STLC.agda
index db11684..693b7b7 100644
--- a/examples/STLC.agda
+++ b/examples/STLC.agda
@@ -17,6 +17,7 @@ open import Data.Vec.Base as Vec using (Vec)
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.List.Sized.Interface
 open import Data.Product using (_×_; _,_; uncurry; ∃; proj₁)
+import Effect.Monad.State.Transformer as StateT
 open import Function.Base
 
 open import Relation.Nullary
@@ -117,7 +118,9 @@ instance
   _ = ParserM.monadPlus
   _ = ParserM.monad
 
-P = ParserM.param [ Token ] (λ n → [ Vec Token n ]) λ where (p , _) _ → Value (_ , lift (p , []))
+P = ParserM.param [ Token ] (λ n → [ Vec Token n ]) λ
+  where (p , _) .StateT.runStateT _ → Value (lift (p , []) , _)
+
 
 theTok : Tok → ∀[ Parser P [ Token ] ]
 theTok t = maybeTok $ λ where
diff --git a/examples/Vec.agda b/examples/Vec.agda
index 03f07ff..83d0410 100644
--- a/examples/Vec.agda
+++ b/examples/Vec.agda
@@ -1,11 +1,13 @@
+{-# OPTIONS --guardedness #-}
+
 module Vec where
 
 open import Text.Parser
 open import Data.Unit.Base
 open import Data.Vec hiding (replicate)
-open import Data.Maybe
-open import Data.Nat
-open import Data.Product
+open import Data.Maybe.Base
+open import Data.Nat.Base hiding (_!)
+open import Data.Product.Base
 
 n-times : {A : Set} → ∀[ Parser A ⇒ Parser (∃[ n ] Vec A (suc n)) ]
 n-times p = decimalℕ &>>= λ n → box (replicate (suc n) p)

From 87e745ea3dea7ab65a83ce99ef78838d0c0e3ba0 Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 5 Aug 2025 16:47:28 +0100
Subject: [PATCH 15/15] [ doc ] update README

---
 README.md | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 1687a70..1b8a39d 100644
--- a/README.md
+++ b/README.md
@@ -7,11 +7,9 @@ The motivation and design decisions behind agdarsec are detailed in:
 
 ## Compilation
 
-[![Travis Status](https://api.travis-ci.org/gallais/agdarsec.svg?branch=master)](https://travis-ci.org/gallais/agdarsec)
-
 To typecheck and compile this project you will need:
 
-* Agda version 2.6.2
+* Agda version 2.6.4.3
 * Agda's standard library (version 2.0)
 
 ## Ports