Minor fixes and faster apologies
"Minor" in physical representation, "major" in spirit. - person coping with writing code after a while
Was adding a single word sorry
, but discovered a few bugs on the way:
val myCorrectTheorem = Theorem(() |- P(x)) {
sorry
showCurrentProof()
}
show
sorry
simply expands to have(thesis) by Sorry
, which is a handful to write when I'm washing my hands free of responsibility for a proof.
Fixes:
sequantable
to sequentable
because I saw it somewhere
show
on theorems now checks for sorry
usage and prints with a different colour, same as the default theorem printing
showCurrentProof
was failing as it relied on Theorem.repr
, which raises a null
exception. Changed to use prettyGoal