modified: qt_interface.py

leanprover-community / lean-client-python

Python talking to the Lean theorem prover

Apache License 2.0

39 stars 6 forks source link

modified: qt_interface.py #10

Closed FredericLeRoux closed 4 years ago

FredericLeRoux commented 4 years ago

The use of curly brackets was previously entailing a KeyError, due to interference with the placeholder {}.

PatrickMassot commented 4 years ago

When we discussed this by email I didn't remember this was a two steps process with sorry being replaced by {} and then the string formatting step. You could also keep sorry instead of REPLACE_ME except if you really want to replace only the first sorry. But, in the context of this little demo, I don't see what multiple sorries would buy you.

PatrickMassot commented 4 years ago

Thanks!