Closed justinchiu-cohere closed 6 days ago
COPRA built a python wrapper for lean/repl.
this commit does the minimal changes to get it running.
setup lean (elan, lean 4.8.0, repl) with
bash scripts/setup_lean.sh
test with
python src/tools/lean4_sync_executor.py
note: i heard some students at stanford built a really nice python wrapper for lean. going to see if we can use that instead.
update: the pypantograph library looks pretty nice: https://github.com/lenianiva/PyPantograph/pull/10
COPRA built a python wrapper for lean/repl.
this commit does the minimal changes to get it running.
setup lean (elan, lean 4.8.0, repl) with
test with
note: i heard some students at stanford built a really nice python wrapper for lean. going to see if we can use that instead.
update: the pypantograph library looks pretty nice: https://github.com/lenianiva/PyPantograph/pull/10