From 2af7bf1b54d04f90477f1c09ab498a2ce5fa7865 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Aug 2022 11:12:19 -0700 Subject: [PATCH] chore: fix link at `src/Lean/Server/README.md` cc @digama0 --- src/Lean/Server/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/README.md b/src/Lean/Server/README.md index 83684e672b..b6d1a0d013 100644 --- a/src/Lean/Server/README.md +++ b/src/Lean/Server/README.md @@ -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