Closed LuoKaiGSW closed 1 month ago
When I trace https://github.com/yangky11/miniF2F-lean4, an error occurs at the following location: https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/interaction/dojo.py#L163 I would like to ask if this Lean4Repl.lean is necessary? Thank you!
When I trace https://github.com/yangky11/miniF2F-lean4, an error occurs at the following location: https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/interaction/dojo.py#L163 I would like to ask if this Lean4Repl.lean is necessary? Thank you!