Merge pull request #106 from mhuisi/lean-pr-testing-7087

chore: adapt for leanprover/lean4#7087
leanprover-community · Feb 23, 2025 · 6b234dc · 6b234dc
2 parents 3011328 + 95d1fcf
commit 6b234dc
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/ProofWidgets/Cancellable.lean b/ProofWidgets/Cancellable.lean
@@ -34,9 +34,9 @@ def mkCancellable [RpcEncodable β] (handler : α → RequestM (RequestTask β))
     α → RequestM (RequestTask RequestId) := fun a => do
   RequestM.asTask do
     let t ← handler a
-    let t' := t.map (·.map rpcEncode)
+    let t' := t.mapCheap (·.map rpcEncode)
     runningRequests.modifyGet fun (id, m) =>
-      (id, (id+1, m.insert id ⟨t', IO.cancel t⟩))
+      (id, (id+1, m.insert id ⟨t'.task, t.cancel⟩))
 
 /-- Cancel the request with ID `rid`.
 Does nothing if `rid` is invalid. -/