leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

Extract type information from info tree #12

Closed insightmind closed 2 years ago

insightmind commented 2 years ago

Description

This PR aims to extract top-level-identifier and type information out of the info tree, so we can use this to display additional information in Alectryon. This is not yet implemented in Alectryon but we aim to implement it in the near future.

Notable Changes

Additional Notes