search

leanprover-community / lean-client-python

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

Fix the example lean file's location of add_comm. #17

Closed Julian closed 3 years ago

Julian commented 3 years ago

I'm assuming the intention was for this file to run, not error, but if indeed this was intentional to demonstrate what happens when there's a problem, obviously let me know.

(For now this is part of fixing #16 )

jasonrute commented 3 years ago

I thought this used to run. Maybe lean changed. I think the intention was to use the example here, but I doubt it matters too much as long as it works.

PatrickMassot commented 3 years ago

Yes, it's meant to work and it did work. Let's merge that as soon as we get back to a globally working state (I don't remember exactly how this file was meant to be used so I don't fancy merging blindly).

Julian commented 3 years ago

Looks like that lean web example also uses nat.add_comm, guess it maybe was originally in the global namespace and was moved to nat?

bryangingechen commented 3 years ago

Looks like that lean web example also uses nat.add_comm, guess it maybe was originally in the global namespace and was moved to nat?

That's correct. It happened when lots of algebra was moved from Lean 3.13.0c to mathlib.

jasonrute commented 3 years ago

I'm just going to merge this. The file is for the trio server example. The example still "work", but gives weird examples with this file broken.