// FIXED FOR NOW, MAYBE.
object HOL2 {
  sealed abstract class prop
  final case class      Holds() extends prop
  final case class      trueprop(x0: Boolean) extends prop
  
  // ECLIPSE WARNING: match may not be exhaustive. It would fail on the  
  // following input: 
  //   (trueprop(true), trueprop(false))
  // Dude, exactly, it's impossible to make a false statement at the prop
  // level of logic. Exceptions are acceptable, but meta-logic false is 
  // semantically offensive to those in the know.
  def follows(p: prop, pa: prop): prop = (p, pa) match {
    case (p, Holds()) => Holds()
    case (Holds(), trueprop(true)) => Holds()
    case (trueprop(false), trueprop(true)) => Holds()
    case (trueprop(true), trueprop(true)) => Holds()
    case (trueprop(false), trueprop(false)) => Holds()
  } 
    
  def hnot(p: prop): prop = follows(p, trueprop(false))
                                                  
  // Return value of Holds(). It's legit, is it not?
  val x = hnot(trueprop(false))
  
  // No error. Simple assignment. I'm not making any logical claim.
  val y = trueprop(false)
  
  // Throws exception. Not because or "trueprop", but because of "follows". 
  // That's what I want for now. Concerning the future, maybe not.
  val z = hnot(trueprop(true))
}


// ORIGINAL: THROWS EXCEPTION FOR A LEGIT STATEMENT.
object HOL {
	sealed abstract class prop
	final case class      Holds extends prop

  def trueprop(x0: Boolean): prop = x0 match {
    case true => Holds()
  }

  def follows(p: prop, pa: prop): prop = (p, pa) match {
    case (p, Holds()) => Holds()
    case (Holds(), p) => p
  }

  def hnot(p: prop): prop = follows(p, trueprop(false))
  
  // Throws exception. This is not where it should throw the exception, because
  // hnot(false) should be an acceptable statement.
  val x = trueprop(false)
}