From 19a701e5c9d2afb98374204ec28f59bf253d8841 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 21 Nov 2024 19:30:28 +0100 Subject: [PATCH] refactor: one more recursive structure (#6159) --- src/Lean/Language/Basic.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 7107ed789484..db975b482cec 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -198,18 +198,13 @@ def withAlwaysResolvedPromises [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] for asynchronously collecting information about the entirety of snapshots in the language server. The involved tasks may form a DAG on the `Task` dependency level but this is not captured by this data structure. -/ -inductive SnapshotTree where - /-- Creates a snapshot tree node. -/ - | mk (element : Snapshot) (children : Array (SnapshotTask SnapshotTree)) +structure SnapshotTree where + /-- The immediately available element of the snapshot tree node. -/ + element : Snapshot + /-- The asynchronously available children of the snapshot tree node. -/ + children : Array (SnapshotTask SnapshotTree) deriving Inhabited -/-- The immediately available element of the snapshot tree node. -/ -abbrev SnapshotTree.element : SnapshotTree → Snapshot - | mk s _ => s -/-- The asynchronously available children of the snapshot tree node. -/ -abbrev SnapshotTree.children : SnapshotTree → Array (SnapshotTask SnapshotTree) - | mk _ children => children - /-- Produces trace of given snapshot tree, synchronously waiting on all children. -/ partial def SnapshotTree.trace (s : SnapshotTree) : CoreM Unit := go none s