lenianiva / PyPantograph

A Machine-to-Machine Interaction System for Lean 4.
https://lenianiva.github.io/PyPantograph/
Apache License 2.0
14 stars 4 forks source link

Documentation of PyPantograph #9

Closed slimtune2023 closed 5 months ago

slimtune2023 commented 5 months ago

Hello! I was wondering if there was any documentation available for using the pantograph server, specifically on the different possible errors one can get when using it. Thank you!

lenianiva commented 5 months ago

There isn't beyond what is provided in the Exception object that ServerError inherits from. I'll add more documentations after NeurIPS if I have time.

slimtune2023 commented 5 months ago

Thank you! I will use the error messages for now.

lenianiva commented 3 weeks ago

There are documentations now, along with examples.