search

leanprover-community / lean-client-python

Python talking to the Lean theorem prover
Apache License 2.0
39 stars 6 forks source link

Support lean command line parameters #9

Closed jasonrute closed 4 years ago

jasonrute commented 4 years ago

This closes Issue #7 . One can enter lean command line parameters as follows:

TrioLeanServer(nursery, lean_cmd = ["lean", "-D", "pp.all=true"])

This is one of a few ways to do it and I'm open to other suggestions.

I'm also open to adding an example usage or even a test if we feel it is helpful.

PatrickMassot commented 4 years ago

I think this is good enough for now.