From b6c3f7d8fdc93fa8304eb1e9b3d7117656e24dc5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 8 Apr 2025 10:54:23 -0700
Subject: [PATCH] chore: Update Lean to v4.18.0

---
 Pantograph/Delate.lean      | 2 +-
 Pantograph/Environment.lean | 4 ++--
 Pantograph/Goal.lean        | 2 +-
 Repl.lean                   | 4 ++--
 Test/Common.lean            | 4 ++--
 Test/Proofs.lean            | 2 +-
 lean-toolchain              | 2 +-
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index b6e016c..a745854 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -26,7 +26,7 @@ def analyzeProjection (env: Environment) (e: Expr): Projection :=
     | _ => panic! "Argument must be proj"
   if (getStructureInfo? env typeName).isSome then
     let ctor := getStructureCtor env typeName
-    let fieldName := getStructureFields env typeName |>.get! idx
+    let fieldName := (getStructureFields env typeName)[idx]!
     let projector := getProjFnForField? env typeName fieldName |>.get!
     .field projector ctor.numParams
   else
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index 3907105..4f0a678 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -26,7 +26,7 @@ def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[
 def module_of_name (env: Environment) (name: Name): Option Name := do
   let moduleId ← env.getModuleIdxFor? name
   if h : moduleId.toNat < env.allImportedModuleNames.size then
-    return env.allImportedModuleNames.get moduleId.toNat h
+    return env.allImportedModuleNames[moduleId.toNat]
   else
     .none
 
@@ -75,7 +75,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
   let info? := env.find? name
   let .some info := info? | Protocol.throw $ Protocol.errorIndex s!"Symbol not found {args.name}"
   let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat)
+    (λ idx => env.allImportedModuleNames[idx.toNat]?)
   let value? := match args.value?, info with
     | .some true, _ => info.value?
     | .some false, _ => .none
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 9af1740..7f135f5 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -102,7 +102,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
 
 @[export pantograph_goal_state_focus]
 protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
-  let goal ← state.savedState.tactic.goals.get? goalId
+  let goal ← state.savedState.tactic.goals[goalId]?
   return {
     state with
     savedState := {
diff --git a/Repl.lean b/Repl.lean
index bcbe8f9..a735c88 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -62,7 +62,7 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
       let desc ← ex.toMessageData.toString
       return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
   if let .some token := cancelTk? then
-    runCancelTokenWithTimeout token (timeout := .mk options.timeout)
+    runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout)
   let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
     | Except.error (Exception.error _ msg)   => Protocol.throw $ { error := "core", desc := ← msg.toString }
     | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
@@ -290,7 +290,7 @@ def execute (command: Protocol.Command): MainM Json := do
     let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
       Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
-    let .some goal := goalState.goals.get? args.goalId |
+    let .some goal := goalState.goals[args.goalId]? |
       Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
     let nextGoalState?: Except _ TacticResult ← liftTermElabM do
       -- NOTE: Should probably use a macro to handle this...
diff --git a/Test/Common.lean b/Test/Common.lean
index c32d62d..c8ffa5d 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -67,8 +67,8 @@ protected def Goal.devolatilize (goal: Goal): Goal :=
 
 end Condensed
 
-def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
-def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
+def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
+def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
 
 def TacticResult.toString : TacticResult → String
   | .success state => s!".success ({state.goals.length} goals)"
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index a760eb4..ceb8690 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -328,7 +328,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
+  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!])
   let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
diff --git a/lean-toolchain b/lean-toolchain
index 5499a24..b2153cd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0