commit: de99c8015a547bcd8baa91852970a2e15cda2abf

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Thu Feb 06 14:11:53 2025 +1100
committer: GitHub <noreply@github.com>

Thu Feb 06 03:11:53 2025 +0000
tree: cf6f6bca6693d4c735f5273270c7781aae3627a2
parent: 49297f12a522100b10422770ad23e89c6f3112c0 [diff]

feat: `#info_trees in` command (#6964)

This PR adds a convenience command `#info_trees in`, which prints the
info trees generated by the following command. It is useful for
debugging or learning about `InfoTree`.

src/Init/Notation.lean[diff]
src/Lean/Elab.lean[diff]
src/Lean/Elab/InfoTrees.lean[Added - diff]
tests/lean/run/info_trees.lean[Added - diff]

4 files changed

tree: cf6f6bca6693d4c735f5273270c7781aae3627a2

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).