aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
281 stars 16 forks source link

Implement `:i` in repl #1125

Closed ice1000 closed 4 months ago

ice1000 commented 4 months ago

It should take the name of a definition, and pretty print it. For constructors or other sub-level definitions, it should pretty print the associated data or owner level definition. In the future, we also need to print class hierarchy, the implemented classes of datas, etc..