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/flake.lock b/flake.lock
index 11c740e..d09589f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
"nixpkgs-lib": "nixpkgs-lib"
},
"locked": {
- "lastModified": 1741352980,
- "narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=",
+ "lastModified": 1743550720,
+ "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
"owner": "hercules-ci",
"repo": "flake-parts",
- "rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9",
+ "rev": "c621e8422220273271f52058f618c94e405bb0f5",
"type": "github"
},
"original": {
@@ -44,11 +44,11 @@
]
},
"locked": {
- "lastModified": 1741472588,
- "narHash": "sha256-XnMeMZKuspEphP+fEq4soc3PY7Nz+gsMPjlsXbobyrA=",
+ "lastModified": 1743534244,
+ "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
"owner": "lenianiva",
"repo": "lean4-nix",
- "rev": "cffeb67d58e02b50ccb9acd51b0212dc653ed6ce",
+ "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
"type": "github"
},
"original": {
@@ -59,11 +59,11 @@
},
"nixpkgs": {
"locked": {
- "lastModified": 1742751704,
- "narHash": "sha256-rBfc+H1dDBUQ2mgVITMGBPI1PGuCznf9rcWX/XIULyE=",
+ "lastModified": 1743975612,
+ "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
"owner": "nixos",
"repo": "nixpkgs",
- "rev": "f0946fa5f1fb876a9dc2e1850d9d3a4e3f914092",
+ "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
"type": "github"
},
"original": {
@@ -75,11 +75,11 @@
},
"nixpkgs-lib": {
"locked": {
- "lastModified": 1740877520,
- "narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=",
+ "lastModified": 1743296961,
+ "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
"owner": "nix-community",
"repo": "nixpkgs.lib",
- "rev": "147dee35aab2193b174e4c0868bd80ead5ce755c",
+ "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
"type": "github"
},
"original": {
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