search

nomeata / incredible

The Incredible Proof Machine
MIT License
359 stars 36 forks source link

Pretty-printer captures constant #69

Closed Rokhan closed 8 years ago

Rokhan commented 8 years ago

Hello,

It seems like a bug to me but it could also be a misleading display of error with a wrong proof.

incredible-proof__bug

Thanks for this software, it's incredibly fun.

nomeata commented 8 years ago

Indeed, this is a problem in the printing of propositions: The left term on the red connection should be something like ∀x₁.P(x), i.e. the bound variable is different from the one in P.

Thanks for this software, it's incredibly fun.

Thanks!