From 812038c69ff1522cbc1b012e09281b72484f8dfd Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Thu, 8 Aug 2024 11:38:00 +0200
Subject: [PATCH] chore: update CI matrix and compatibility (#38)

Supports generalized `Lean.Parsec`
---
 .github/workflows/ci.yml                  | 3 ++-
 src/compat/SubVerso/Compat.lean           | 3 +++
 src/examples/SubVerso/Examples/Slice.lean | 7 +++++--
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6dda2c8..c30aa0c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -17,7 +17,8 @@ jobs:
           - "4.8.0"
           - "4.9.0"
           - "4.10.0"
-          - "nightly-2024-08-03"
+          - "4.11.0-rc1"
+          - "nightly-2024-08-08"
         platform:
           - os: ubuntu-latest
             installer: |
diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
index 50a4e0e..b04a960 100644
--- a/src/compat/SubVerso/Compat.lean
+++ b/src/compat/SubVerso/Compat.lean
@@ -57,3 +57,6 @@ def refIdentCase (ri : Lsp.RefIdent)
     | .fvar id => onFVar id
     | .const x => onConst x
   ]
+
+abbrev Parsec (α : Type) : Type :=
+  %first_succeeding [(Lean.Parsec α : Type), (Lean.Parsec String.Iterator α : Type)]
diff --git a/src/examples/SubVerso/Examples/Slice.lean b/src/examples/SubVerso/Examples/Slice.lean
index f45fe39..43e4d6a 100644
--- a/src/examples/SubVerso/Examples/Slice.lean
+++ b/src/examples/SubVerso/Examples/Slice.lean
@@ -7,9 +7,12 @@ import Lean.Data.Parsec
 import Lean.Data.Position
 import Lean.Syntax
 import Lean.Elab.Command
+import SubVerso.Compat
 import SubVerso.Examples.Slice.Attribute
 
-open Lean
+
+open Lean hiding Parsec
+open SubVerso.Compat (Parsec)
 
 namespace SubVerso.Examples.Slice
 
@@ -68,7 +71,7 @@ deriving Repr
 private def SliceCommand.beginRange := SliceCommand.mk true
 private def SliceCommand.endRange := SliceCommand.mk false
 
-open Parsec in
+open Lean.Parsec String in
 private def sliceCommand (range : String.Range) : Parsec SliceCommand := do
   ws
   skipString "!!"