package imperative
- Alphabetic
- Public
- All
Type Members
- case class Assume(name: LocalName, tp: Term) extends ProofStep with Product with Serializable
- case class Cases(splitOn: Term, cases: List[(Term, ImperativeProof)]) extends ProofStep with Product with Serializable
- case class Hence(tp: Term, by: ImperativeProof, name: Option[LocalName]) extends ProofStep with Product with Serializable
- case class ImperativeProof(steps: List[ProofStep]) extends Product with Serializable
- case class Let(name: List[LocalName], tp: Option[Term], df: Term) extends ProofStep with Product with Serializable
- case class LocalRef(name: LocalName) extends ProofStep with Product with Serializable
- class ProofState extends AnyRef
- abstract class ProofStep extends AnyRef
- abstract class ProofStepRule extends AnyRef
- case class ProofTerm(pf: Term) extends ProofStep with Product with Serializable
- class Prover extends AnyRef
- case class Suffices(newGoal: Term, by: ImperativeProof) extends ProofStep with Product with Serializable
Value Members
- object CasesRule extends ProofStepRule