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

chore: fix link at src/Lean/Server/README.md

Browse source 
cc @digama0
This commit is contained in:
Leonardo de Moura 2022-08-01 11:12:19 -07:00
parent 5a8ee410b1
commit 2af7bf1b54
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/README.md
View file

@ -54,7 +54,7 @@ After the snapshot is available, they can access its data, in particular the com
The `InfoTree` is the second central server data structure.
It is filled during elaboration with various metadata that cannot (easily) be recovered from the kernel declarations in the environment: goal & subterm infos including the precise local & metavariable contexts used during elaboration, macro expansion steps, ...
Once a relevant `Snapshot` `snap` has been located, `snap.infoTree.smallestInfo?` and other functions from `Lean.Server.InfoUtils` can be used to further locate information about a document position.
The test `tests/lean/infoTree.lean` shows how to inspect the info tree of a command right in the editor.
The command `set_option trace.Elab.info true` instructs Lean to display the `InfoTree` for the declarations occurring after it.
## Code style