abstract class Term+
−
case class Var(s: String) extends Term+
−
case class Consts(s: String) extends Term+
−
case class Fun(s: String, ts: List[Term]) extends Term+
−
+
−
abstract class Form+
−
case object True extends Form+
−
case object False extends Form+
−
case class And(f1: Form, f2: Form) extends Form+
−
case class Or(f1: Form, f2: Form) extends Form+
−
case class Imp(f1: Form, f2: Form) extends Form+
−
case class Neg(f: Form) extends Form+
−
case class Pred(s: String, ts: List[Term]) extends Form+
−
+
−
case class Judgement(Gamma: List[Form], F: Form) {+
−
  def lhs = Gamma+
−
  def rhs = F+
−
}+
−