search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
478 stars 72 forks source link

Handle the Breaking Changes to `InfoTree` in `v4.6.0-rc1` #132

Closed yangky11 closed 4 months ago

yangky11 commented 5 months ago

See https://github.com/leanprover/lean4/pull/3159

To reproduce:

from lean_dojo import *

repo = LeanGitRepo("https://github.com/leanprover/std4", "7969a8724ba0c31716c56e551c51a048a8537725")
trace(repo)
Peiyang-Song commented 5 months ago

PR: #134