max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: one more recursive structure (#6159)

Browse source
This commit is contained in:
Sebastian Ullrich 2024-11-21 19:30:28 +01:00 • committed by GitHub
parent fc4305ab15
commit 19a701e5c9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Language/Basic.lean
View file

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