package simp
Content Hierarchy
Ordering
- Alphabetic
Visibility
- Public
- Protected
Type Members
- case class AtomSimpLemma(proj: SimpLemmaProjection) extends SimpProc with Product with Serializable
- case class EqSimpLemma(proj: SimpLemmaProjection) extends SimpProc with Product with Serializable
- case class IffSimpLemma(proj: SimpLemmaProjection) extends SimpProc with Product with Serializable
- case class NegAtomSimpLemma(proj: SimpLemmaProjection) extends SimpProc with Product with Serializable
- sealed trait SimpEqResult extends AnyRef
- sealed trait SimpIffResult extends AnyRef
- case class SimpLemmaProjection(proof: LKProof, conds: HOLSequent, idx: SequentIndex, fixed: PreSubstitution) extends Product with Serializable
- trait SimpProc extends AnyRef
- case class SimpTactic(onLabel: Option[String] = None, extraLemmasList: Seq[String] = Seq(), excludedLemmasList: Set[String] = Set(), useAssumptions: Boolean = false)(implicit ctx: Context) extends Tactical1[Unit] with Product with Serializable
- case class Simplifier(lemmas: Seq[SimpProc]) extends Product with Serializable
Value Members
- case object QPropSimpProc extends SimpProc with Product with Serializable
- object SimpEqResult
- object SimpIffResult
- object SimpLemmas
- object SimpProver extends OneShotProver
- object Simplifier extends Serializable
This is the API documentation for GAPT.
The main package is gapt.