diff -r 4e108563716c -r 10526c967679 programs/prove1.scala --- a/programs/prove1.scala Tue Nov 12 08:03:16 2013 +0000 +++ b/programs/prove1.scala Tue Nov 12 09:57:22 2013 +0000 @@ -31,17 +31,18 @@ val goal = Judgement(Gamma, Del) // request: provable or not? +def partitions[A](ls: List[A]): List[(A, List[A])] = + ls.map (s => (s, ls diff List(s))) + + def prove(j: Judgement, sc: () => Unit) : Unit = { if (j.lhs.contains(j.rhs)) sc() // Axiom rule else prove1(j.lhs, j.rhs, sc) } -def partitions[A](ls: List[A]): List[(A, List[A])] = - ls.map (s => (s, ls diff List(s))) - def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = rhs match { - case True => sc() + case True => sc () case False => () case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) case Says(p, f1) => prove(Judgement(lhs, f1), sc)