Proof judgement ADT, sugars and printer
Compare changes
Created by: FlorianCassayre
sealed abstract class SCProofCheckerJudgement:
def isValid: Boolean
case object SCValidProof extends SCProofCheckerJudgement
case class SCInvalidProof(path: Seq[Int], message: String) extends SCProofCheckerJudgement
Structurally equivalent to an Option[(Seq[Int], String)]
, but makes more sense.
The negative indices weren't aligned with the rest (this was introduced by a careless copy paste).
Added the following missing syntactic sugars:
formula match
case a ==> b => ...
case a <=> b => ...
() |- (a, b)