This commit is contained in:
2
.gitignore
vendored
2
.gitignore
vendored
@@ -1 +1,3 @@
|
||||
/.lake
|
||||
/asyncio
|
||||
/Basic_aristotle.lean
|
||||
|
||||
@@ -1,9 +1,11 @@
|
||||
#!/usr/bin/python
|
||||
|
||||
import asyncio
|
||||
import aristotlelib
|
||||
|
||||
async def main():
|
||||
# Prove a theorem from a Lean file
|
||||
solution_path = await aristotlelib.Project.prove_from_file("/home/kebekus/Mathe/aristotle/Basic.lean")
|
||||
solution_path = await aristotlelib.Project.prove_from_file("/home/kebekus/Mathe/aristotle/Aristotle/Basic.lean")
|
||||
print(f"Solution saved to: {solution_path}")
|
||||
|
||||
asyncio.run(main())
|
||||
|
||||
Reference in New Issue
Block a user