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

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

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 := {

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...

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)"

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0