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..e8f6646 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 α : Type)] diff --git a/src/examples/SubVerso/Examples/Slice.lean b/src/examples/SubVerso/Examples/Slice.lean index f45fe39..131c06a 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 in private def sliceCommand (range : String.Range) : Parsec SliceCommand := do ws skipString "!!"