gaptic

package gaptic

Source: package.scala

Linear Supertypes

TacticCommands, AnyRef, Any

Content Hierarchy

Ordering

Alphabetic
By Inheritance

Inherited

gaptic
TacticCommands
AnyRef
Any

Hide All
Show All

Visibility

Public
Protected

Package Members

package tactics

Type Members

trait BinaryTactic[+T] extends Tactic[T]
Trait for tactics that create two new subgoals.
Trait for tactics that create two new subgoals. Provides the left and right methods.
final case class CanLabelledSequent(labelledSequent: Sequent[(String, Formula)]) extends AnyVal with Product with Serializable
trait LemmaHelper[T] extends AnyRef
case class OnLabel(label: String) extends TacticApplyMode with Product with Serializable
Apply a tactic to a specific label.
Apply a tactic to a specific label.
label
The label that the tactic should be applied to.
case class OpenAssumption(labelledSequent: Sequent[(String, Formula)], index: OpenAssumptionIndex = new OpenAssumptionIndex) extends InitialSequent with Product with Serializable
Defines the case class open assumption which considers an arbitrary labelled sequence an axiom.
class OpenAssumptionIndex extends AnyRef
The globally unique index of an open assumption in a proof state.
case class ProofState extends Product with Serializable
class QedFailureException extends Exception
trait SimpleLemmaHelper[T] extends LemmaHelper[T]
trait Tactic[+T] extends AnyRef
sealed abstract class TacticApplyMode extends AnyRef
Class that describes how a tactic should be applied: to a label, to the unique fitting formula, or to any fitting formula.
trait TacticBlockArgument[T] extends SimpleLemmaHelper[T]
trait TacticCommands extends AnyRef
implicit final class TacticEitherOps[T, E] extends AnyVal
case class TacticFailure(tactic: Tactic[_], state: Option[ProofState], message: String) extends Product with Serializable
class TacticFailureException extends Exception
case class TacticFailureFailureException(error: TacticFailure)(implicit sig: BabelSignature) extends TacticFailureException with Product with Serializable
implicit final class TacticOptionOps[T] extends AnyVal
trait Tactical[+T] extends Tactic[T]
trait Tactical1[+T] extends Tactic[T]
class TacticsProof extends TacticsProof0
class TacticsProof0 extends AnyRef

Value Members

def allL(terms: Expr*): ForallLeftTactic
Applies the ForallLeft tactic to the current subgoal: The goal
Applies the ForallLeft tactic to the current subgoal: The goal
∀x₁,...,∀x_n.A, Γ :- Δ
is reduced to
A[x₁\t₁,...,x_n\t_n], ∀x₁,...,∀x_n.A, Γ :- Δ.
This will only work if there is exactly one universal formula in the antecedent!
terms
The terms t₁,...,t_n.
Definition Classes
TacticCommands
def allL(applyToLabel: String, terms: Expr*): ForallLeftTactic
Applies the ForallLeft tactic to the current subgoal: The goal
Applies the ForallLeft tactic to the current subgoal: The goal
∀x₁,...,∀x_n.A, Γ :- Δ
is reduced to
A[x₁\t₁,...,x_n\t_n], ∀x₁,...,∀x_n.A, Γ :- Δ.
applyToLabel
The label of the formula ∀x₁,...,∀x_n.A.
terms
The terms t₁,...,t_n.
Definition Classes
TacticCommands
def allR: ForallRightTactic
Applies the ForallRight tactic to the current subgoal: The goal
Applies the ForallRight tactic to the current subgoal: The goal
Γ :- Δ, ∀x.A
is reduced to
Γ :- Δ, A.
This will only work if there is exactly one universal formula in the succedent!
Definition Classes
TacticCommands
def allR(applyToLabel: String): ForallRightTactic
Applies the ForallRight tactic to the current subgoal: The goal
Applies the ForallRight tactic to the current subgoal: The goal
Γ :- Δ, ∀x.A
is reduced to
Γ :- Δ, A.
applyToLabel
The label of the formula ∀x.A.
Definition Classes
TacticCommands
def allR(eigenVariable: Var): ForallRightTactic
Applies the ForallRight tactic to the current subgoal: The goal
Applies the ForallRight tactic to the current subgoal: The goal
Γ :- Δ, ∀x.A
is reduced to
Γ :- Δ, A[x\α].
This will only work if there is exactly one universal formula in the succedent!
eigenVariable
The variable α.
Definition Classes
TacticCommands
def allR(applyToLabel: String, eigenVariable: Var): ForallRightTactic
Applies the ForallRight tactic to the current subgoal: The goal
Applies the ForallRight tactic to the current subgoal: The goal
Γ :- Δ, ∀x.A
is reduced to
Γ :- Δ, A[x\α].
applyToLabel
The label of the formula ∀x.A.
eigenVariable
The variable α.
Definition Classes
TacticCommands
def anaInd(implicit ctx: Context): Tactic[Unit]
Definition Classes
TacticCommands
def anaIndG(implicit ctx: Context): Tactic[Unit]
Definition Classes
TacticCommands
def analyticInduction(implicit ctx: MutableContext): AnalyticInductionTactic
Definition Classes
TacticCommands
def andL: AndLeftTactic
Applies the AndLeft tactic to the current subgoal: The goal
Applies the AndLeft tactic to the current subgoal: The goal
A ∧ B, Γ :- Δ
is reduced to
A, B, Γ :- Δ.
This will only work if there is exactly one conjunctive formula in the antecedent!
Definition Classes
TacticCommands
def andL(applyToLabel: String): AndLeftTactic
Applies the AndLeft tactic to the current subgoal: The goal
Applies the AndLeft tactic to the current subgoal: The goal
A ∧ B, Γ :- Δ
is reduced to
A, B, Γ :- Δ.
applyToLabel
The label of the formula A ∧ B.
Definition Classes
TacticCommands
def andR: AndRightTactic
Applies the AndRight tactic to the current subgoal: The goal
Applies the AndRight tactic to the current subgoal: The goal
Γ :- Δ, A ∧ B
is reduced to
Γ :- Δ, A and Γ :- Δ, B.
This will only work if there is exactly one conjunctive formula in the succedent!
Definition Classes
TacticCommands
def andR(applyToLabel: String): AndRightTactic
Applies the AndRight tactic to the current subgoal: The goal
Applies the AndRight tactic to the current subgoal: The goal
Γ :- Δ, A ∧ B
is reduced to
Γ :- Δ, A and Γ :- Δ, B.
applyToLabel
The label of the formula A ∧ B.
Definition Classes
TacticCommands
def axiomBot: BottomAxiomTactic
Applies the BottomAxiom tactic to the current subgoal: A subgoal of the form ⊥, Γ :- Δ will be closed.
Applies the BottomAxiom tactic to the current subgoal: A subgoal of the form ⊥, Γ :- Δ will be closed.
Definition Classes
TacticCommands
def axiomLog: LogicalAxiomTactic
Applies the LogicalAxiom tactic to the current subgoal: A subgoal of the form A, Γ :- Δ, A will be closed.
Applies the LogicalAxiom tactic to the current subgoal: A subgoal of the form A, Γ :- Δ, A will be closed.
Definition Classes
TacticCommands
def axiomRefl: ReflexivityAxiomTactic
Applies the ReflexivityAxiom tactic to the current subgoal: A subgoal of the form Γ :- Δ, s = s will be closed.
Applies the ReflexivityAxiom tactic to the current subgoal: A subgoal of the form Γ :- Δ, s = s will be closed.
Definition Classes
TacticCommands
def axiomTop: TopAxiomTactic
Applies the TopAxiom tactic to the current subgoal: A subgoal of the form Γ :- Δ, ⊤ will be closed.
Applies the TopAxiom tactic to the current subgoal: A subgoal of the form Γ :- Δ, ⊤ will be closed.
Definition Classes
TacticCommands
def by: TacticBlockArgument[Tactic[Unit]]
by { tac1; tac2; ...; tacn } solves the first goal using the provided tactic block, and fails otherwise
by { tac1; tac2; ...; tacn } solves the first goal using the provided tactic block, and fails otherwise
Definition Classes
TacticCommands
def cases(lemma: String, terms: Expr*)(implicit ctx: Context): Tactic[Unit]
Definition Classes
TacticCommands
def casesW(label: String, lemma: String, terms: Expr*)(implicit ctx: Context): Tactic[Unit]
Definition Classes
TacticCommands
def chain(h: String): ChainTactic
Definition Classes
TacticCommands
def cut(label: String, cutFormula: Formula): CutTactic
Applies the Cut tactic to the current subgoal: The goal
Applies the Cut tactic to the current subgoal: The goal
Γ :- Δ
is reduced to
Γ :- Δ, C and C, Γ :- Δ.
label
The label of C.
cutFormula
The formula C.
Definition Classes
TacticCommands
def decompose: Tactic[Unit]
Decomposes the current subgoal by applying all "simple" rules as often as possible.
Decomposes the current subgoal by applying all "simple" rules as often as possible. These rules are: - ¬:l and ¬:r - ∧:l - ∨:r - →:r - ∀:r - ∃:l
Definition Classes
TacticCommands
def destruct(label: String): Tactic[Any]
Definition Classes
TacticCommands
def eql(eq: String, fm: String): EqualityTactic
Applies the Equality tactic to the current subgoal: Given an equation s = t and a formula A, some occurrences of s in A are replaced by t or vice versa.
Applies the Equality tactic to the current subgoal: Given an equation s = t and a formula A, some occurrences of s in A are replaced by t or vice versa. The exact behavior can be controlled with additional commands:
- fromLeftToRight: Occurrences of s will be replaced by t. - fromRightToLeft: Occurrences of t will be replaced by s. - yielding(f): The tactic will attempt to replace occurences in such a way that the end result is f.
If neither fromLeftToRight nor fromRightToLeft is used, the direction of replacement needs to be unambiguous, i.e. s and t may not both occur in A.
eq
The label of s = t.
fm
The label of A.
Definition Classes
TacticCommands
def escargot(implicit ctx: MutableContext): ResolutionProverTactic
Calls escargot on the current subgoal.
Calls escargot on the current subgoal.
Definition Classes
TacticCommands
def escrgt(implicit ctx: Context): Tactic[Unit]
Definition Classes
TacticCommands
def exL: ExistsLeftTactic
Applies the ExistsLeft tactic to the current subgoal: The goal
Applies the ExistsLeft tactic to the current subgoal: The goal
∃x.A, Γ :- Δ
is reduced to
A, Γ :- Δ.
This will only work if there is exactly one existential formula in the antecedent!
Definition Classes
TacticCommands
def exL(applyToLabel: String): ExistsLeftTactic
Applies the ExistsLeft tactic to the current subgoal: The goal
Applies the ExistsLeft tactic to the current subgoal: The goal
∃x.A, Γ :- Δ
is reduced to
A, Γ :- Δ.
applyToLabel
The label of the formula ∃x.A.
Definition Classes
TacticCommands
def exL(eigenVariable: Var): ExistsLeftTactic
Applies the ExistsLeft tactic to the current subgoal: The goal
Applies the ExistsLeft tactic to the current subgoal: The goal
∃x.A, Γ :- Δ
is reduced to
A[x\α], Γ :- Δ.
This will only work if there is exactly one existential formula in the antecedent!
eigenVariable
The variable α.
Definition Classes
TacticCommands
def exL(applyToLabel: String, eigenVariable: Var): ExistsLeftTactic
Applies the ExistsLeft tactic to the current subgoal: The goal
Applies the ExistsLeft tactic to the current subgoal: The goal
∃x.A, Γ :- Δ
is reduced to
A[x\α], Γ :- Δ.
applyToLabel
The label of the formula ∃x.A.
eigenVariable
The variable α.
Definition Classes
TacticCommands
def exR(terms: Expr*): ExistsRightTactic
Applies the ExistsRight tactic to the current subgoal: The goal
Applies the ExistsRight tactic to the current subgoal: The goal
Γ :- Δ, ∃x₁...∃x_n.A
is reduced to
Γ :- Δ, ∃x₁...∃x_n.A, A[x₁\t₁,...,x_n\t_n].
This will only work if there is exactly one existential formula in the succedent!
terms
The terms t₁,...,t_n.
Definition Classes
TacticCommands
def exR(applyToLabel: String, terms: Expr*): ExistsRightTactic
Applies the ExistsRight tactic to the current subgoal: The goal
Applies the ExistsRight tactic to the current subgoal: The goal
Γ :- Δ, ∃x₁...∃x_n.A
is reduced to
Γ :- Δ, ∃x₁...∃x_n.A, A[x₁\t₁,...,x_n\t_n].
applyToLabel
The label of the formula ∃x₁...∃x_n.A.
terms
The terms t₁,...,t_n.
Definition Classes
TacticCommands
def fail: Tactic[Nothing] { def apply(proofState: gapt.proofs.gaptic.ProofState): scala.util.Left[gapt.proofs.gaptic.TacticFailure,Nothing] }
Tactic that immediately fails.
Tactic that immediately fails.
Definition Classes
TacticCommands
def foTheory(implicit ctx: Context): Tactic[Unit]
Solves the current subgoal as a first-order consequence of the background theory.
Solves the current subgoal as a first-order consequence of the background theory. This closes the goal.
ctx
A gapt.proofs.context.Context. The current subgoal must be contained in its background theory.
Definition Classes
TacticCommands
def focus(indexOfSubGoal: OpenAssumptionIndex): FocusTactic
Moves the specified goal to the front of the goal list.
Moves the specified goal to the front of the goal list.
indexOfSubGoal
The index of the goal.
Definition Classes
TacticCommands
def focus(indexOfSubGoal: Int): FocusTactic
Moves the specified goal to the front of the goal list.
Moves the specified goal to the front of the goal list.
indexOfSubGoal
The index of the goal.
Definition Classes
TacticCommands
def forget(pred: (String, Formula) => Boolean): Tactic[Unit]
Definition Classes
TacticCommands
def forget(ls: String*): Tactic[Unit]
Lets you "forget" a sequence of formulas, i.e.
Lets you "forget" a sequence of formulas, i.e. the tactics version of the weakening rule. The formulas with labels L₁,...,L_n will be removed from the current goal.
ls
The labels L₁,...,_Ln.
Definition Classes
TacticCommands
def forwardChain(lemma: String, target: TacticApplyMode = UniqueFormula, substitution: Map[Var, Expr] = Map()): ForwardChain
Definition Classes
TacticCommands
See also
gapt.proofs.gaptic.tactics.ForwardChain.
def generalize(vs: Var*): Tactic[Unit]
Definition Classes
TacticCommands
def haveInstance(formula: Formula, polarity: Polarity): Tactic[String]
Instantiates prenex quantifiers to obtain a formula in a given polarity.
Instantiates prenex quantifiers to obtain a formula in a given polarity.
Definition Classes
TacticCommands
def haveInstances(sequent: HOLSequent): Tactic[Sequent[String]]
Definition Classes
TacticCommands
def impL: ImpLeftTactic
Applies the ImpLeft tactic to the current subgoal: The goal
Applies the ImpLeft tactic to the current subgoal: The goal
A → B, Γ :- Δ
is reduced to
Γ :- Δ, A and B, Γ :- Δ.
This will only work if there is exactly one implicative formula in the antecedent!
Definition Classes
TacticCommands
def impL(applyToLabel: String): ImpLeftTactic
Applies the ImpLeft tactic to the current subgoal: The goal
Applies the ImpLeft tactic to the current subgoal: The goal
A → B, Γ :- Δ
is reduced to
Γ :- Δ, A and B, Γ :- Δ.
applyToLabel
The label of the formula A → B.
Definition Classes
TacticCommands
def impR: ImpRightTactic
Applies the ImpRight tactic to the current subgoal: The goal
Applies the ImpRight tactic to the current subgoal: The goal
Γ :- Δ, A → B
is reduced to
A, Γ :- Δ, B.
This will only work if there is exactly one implicative formula in the succedent!
Definition Classes
TacticCommands
def impR(applyToLabel: String): ImpRightTactic
Applies the ImpRight tactic to the current subgoal: The goal
Applies the ImpRight tactic to the current subgoal: The goal
Γ :- Δ, A → B
is reduced to
A, Γ :- Δ, B.
applyToLabel
The label of the formula A → B.
Definition Classes
TacticCommands
def include(labels: String*)(implicit ctx: Context, dummyImplicit: DummyImplicit): Tactic[Unit]
Definition Classes
TacticCommands
def include(names: Expr*)(implicit ctx: Context): Tactic[Unit]
Definition Classes
TacticCommands
def include(label: String, proof: LKProof): Tactic[Unit]
Uses an LKProof as a lemma.
Uses an LKProof as a lemma.
If proof ends in Γ :- φ, then the current goal
Γ, Π :- Λ
is reduced to
Γ, Π, φ :- Λ
label
the label for φ in the subgoal
proof
The proof to insert as a lemma by a cut.
Definition Classes
TacticCommands
def induction(on: Var, label: String)(implicit ctx: Context): InductionTactic
Applies the Induction tactic to the current subgoal: The goal
Applies the Induction tactic to the current subgoal: The goal
Γ, :- Δ, ∀x.A
is reduced to n new subgoals, where n is the number of constructors of the type of x.
label
The label of the formula ∀x.A.
ctx
A gapt.proofs.context.Context. It must contain an inductive definition of the type of x.
Definition Classes
TacticCommands
def induction(on: Var)(implicit ctx: Context): InductionTactic
Applies the Induction tactic to the current subgoal: The goal
Applies the Induction tactic to the current subgoal: The goal
Γ, :- Δ, ∀x.A
is reduced to n new subgoals, where n is the number of constructors of the type of x.
This will only work if there is exactly one universal formula in the succedent!
ctx
A gapt.proofs.context.Context. It must contain an inductive definition of the type of x.
Definition Classes
TacticCommands
def insert(proof: LKProof): InsertTactic
Inserts an LKProof for the current subgoal.
Inserts an LKProof for the current subgoal.
proof
The proof to be inserted. Its end-sequent must subsume the current goal.
Definition Classes
TacticCommands
def introUnivsExcept(i: Int): Tactic[Unit]
Definition Classes
TacticCommands
def negL: NegLeftTactic
Applies the NegLeft tactic to the current subgoal: The goal
Applies the NegLeft tactic to the current subgoal: The goal
¬A, Γ :- Δ
is reduced to
Γ :- Δ, A.
This will only work if there is exactly one negated formula in the antecedent!
Definition Classes
TacticCommands
def negL(applyToLabel: String): NegLeftTactic
Applies the NegLeft tactic to the current subgoal: The goal
Applies the NegLeft tactic to the current subgoal: The goal
¬A, Γ :- Δ
is reduced to
Γ :- Δ, A.
applyToLabel
The label of the formula ¬A.
Definition Classes
TacticCommands
def negR: NegRightTactic
Applies the NegRight tactic to the current subgoal: The goal
Applies the NegRight tactic to the current subgoal: The goal
Γ :- Δ, A
is reduced to
A, Γ :- Δ.
This will only work if there is exactly one negated formula in the succedent!
Definition Classes
TacticCommands
def negR(applyToLabel: String): NegRightTactic
Applies the NegRight tactic to the current subgoal: The goal
Applies the NegRight tactic to the current subgoal: The goal
Γ :- Δ, ¬A
is reduced to
A, Γ :- Δ.
applyToLabel
The label of the formula ¬A.
Definition Classes
TacticCommands
def now: Tactic[Unit]
Definition Classes
TacticCommands
def orL: OrLeftTactic
Applies the OrLeft tactic to the current subgoal: The goal
Applies the OrLeft tactic to the current subgoal: The goal
A ∨ B, Γ :- Δ
is reduced to
A, Γ :- Δ and B, Γ :- Δ.
This will only work if there is exactly one disjunctive formula in the antecedent!
Definition Classes
TacticCommands
def orL(applyToLabel: String): OrLeftTactic
Applies the OrLeft tactic to the current subgoal: The goal
Applies the OrLeft tactic to the current subgoal: The goal
A ∨ B, Γ :- Δ
is reduced to
A, Γ :- Δ and B, Γ :- Δ.
applyToLabel
The label of the formula A ∨ B.
Definition Classes
TacticCommands
def orR: OrRightTactic
Applies the OrRight tactic to the current subgoal: The goal
Applies the OrRight tactic to the current subgoal: The goal
Γ :- Δ, A ∨ B
is reduced to
Γ :- Δ, A, B.
This will only work if there is exactly one disjunctive formula in the succedent!
Definition Classes
TacticCommands
def orR(applyToLabel: String): OrRightTactic
Applies the OrRight tactic to the current subgoal: The goal
Applies the OrRight tactic to the current subgoal: The goal
Γ :- Δ, A ∨ B
is reduced to
Γ :- Δ, A, B.
applyToLabel
The label of the formula A ∨ B.
Definition Classes
TacticCommands
def prop: Tactic[Unit]
Calls the builtin tableau prover on the current subgoal.
Calls the builtin tableau prover on the current subgoal. If the goal is a tautology, a proof will automatically be found and inserted.
Definition Classes
TacticCommands
def prover9(implicit ctx: MutableContext): ResolutionProverTactic
Calls prover9 on the current subgoal.
Calls prover9 on the current subgoal.
Definition Classes
TacticCommands
def quasiprop: Tactic[Unit]
Definition Classes
TacticCommands
def ref(proofName: String)(implicit ctx: Context): ProofLinkTactic
Applies the LogicalAxiom tactic to the current subgoal: A subgoal of the form A, Γ :- Δ, A will be closed.
Applies the LogicalAxiom tactic to the current subgoal: A subgoal of the form A, Γ :- Δ, A will be closed.
Definition Classes
TacticCommands
def refl: ReflexivityAxiomTactic
Synonym for axiomRefl.
Synonym for axiomRefl.
Definition Classes
TacticCommands
def renameLabel(oldLabel: String): RenameTactic
Changes the provided label.
Changes the provided label. Syntax:
```
renameLabel("foo") to "bar"
```
oldLabel
The label to be renamed.
Definition Classes
TacticCommands
def repeat[T](t: Tactic[T]): RepeatTactic[T]
Repeats a tactical until it fails.
Repeats a tactical until it fails.
t
A tactical.
Definition Classes
TacticCommands
def resolutionProver(prover: Prover)(implicit ctx: MutableContext): ResolutionProverTactic
Definition Classes
TacticCommands
def revert(hyps: String*): Tactic[Unit]
Definition Classes
TacticCommands
def rewrite: RewriteTactic
Rewrites the formula specified by target using (possibly universally quantified) equations.
Rewrites the formula specified by target using (possibly universally quantified) equations.
```
rewrite.many ltr "equation1" in "target"
rewrite.many ltr ("equation1", "eq2") rtl ("eq3", "eq4") in "target" subst (hov"x" -> le"f(f(c))")
```
ltr: rewrite left-to-right using this equation rtl: rewrite right-to-left using this equation many: rewrite as long as possible (default is to only rewrite once)
Definition Classes
TacticCommands
def simp(implicit ctx: Context): SimpTactic
Definition Classes
TacticCommands
def skip: Tactic[Unit]
Does nothing.
Does nothing.
Definition Classes
TacticCommands
def subst(hyps: String*): Tactic[Unit]
Definition Classes
TacticCommands
def subst1(hyp: String): SubstTactic
Definition Classes
TacticCommands
def subst1: SubstTactic
Definition Classes
TacticCommands
def substAll: Tactic[Unit]
Definition Classes
TacticCommands
def theory(implicit ctx: Context): Tactic[Unit]
Declares the current subgoal as a theory axiom, i.e.
Declares the current subgoal as a theory axiom, i.e. a sequent that is contained in the background theory. This closes the goal.
ctx
A gapt.proofs.context.Context. The current subgoal must be contained in its background theory.
Definition Classes
TacticCommands
def trace(implicit sig: BabelSignature): Tactic[Unit]
Definition Classes
TacticCommands
def treeGrammarInduction(implicit ctx: Context): TreeGrammarInductionTactic
Definition Classes
TacticCommands
def trivial: Tactic[Unit]
Attempts to apply the tactics axiomTop, axiomBot, axiomRefl, and axiomLog.
Attempts to apply the tactics axiomTop, axiomBot, axiomRefl, and axiomLog.
Definition Classes
TacticCommands
def unfold(definitions: String*)(implicit ctx: Context): UnfoldTacticHelper
Replaces a defined constant with its definition.
Replaces a defined constant with its definition. Syntax:
```
unfold("def1", "def2",...,"defn") in ("label1", "label2",...,"labelk")
```
NB: This will only replace the first definition it finds in each supplied formula. If you want to unfold all definitions, use repeat.
definitions
The definitions def1,...,defn.
ctx
A gapt.proofs.context.Context. The definitions you want to unfold need to be present in ctx.
Definition Classes
TacticCommands
case object AnyFormula extends TacticApplyMode with Product with Serializable
Apply a tactic if there is a formula that fits.
object CanLabelledSequent extends Serializable
object IncompleteProof
object Lemma
object LemmaMacros
object NewLabel
object NewLabels
Object that wraps helper function to generate new label from an existing one
object Proof
object ProofState extends Serializable
object Tactic
object TacticCommands extends TacticCommands
Predefined tactics in gaptic.
case object currentGoal extends Tactical1[OpenAssumption] with Product with Serializable
Retrieves the current subgoal.
Retrieves the current subgoal.
Definition Classes
TacticCommands
object TacticFailure extends Serializable
implicit object TacticMonad extends Monad[Tactic]
Implementation of the cats.Monad typeclass for tactics.
case object UniqueFormula extends TacticApplyMode with Product with Serializable
Apply a tactic only if there is exactly one formula that fits.
object guessLabels

Deprecated Value Members

def sorry: Tactic[Unit]
Leaves a hole in the current proof by inserting a dummy proof of the empty sequent.
Leaves a hole in the current proof by inserting a dummy proof of the empty sequent.
Definition Classes
TacticCommands
Annotations
@deprecated
Deprecated
(Since version the dawn of time) Proof not finished!

Packages

gaptic

package gaptic

Package Members

Type Members

Value Members

Deprecated Value Members

Inherited from TacticCommands

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

gaptic

package gaptic

Package Members

Type Members

Value Members

Deprecated Value Members

Inherited from TacticCommands

Inherited from AnyRef

Inherited from Any

Ungrouped

gaptic