search

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
208 stars 44 forks source link

Parser tactic state using LeanDojo parser #21

Closed antonkov closed 1 year ago

antonkov commented 1 year ago

Using parser from https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/interaction/dojo.py as suggested in https://github.com/lean-dojo/ReProver/pull/17#issuecomment-1642200418