refactor: one more recursive structure (#6159)

leanprover · Nov 21, 2024 · 19a701e · 19a701e
1 parent fc4305a
commit 19a701e
Showing 1 changed file with 5 additions and 10 deletions.
diff --git 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