gapt-examples
API
Generated with
gapt-examples/gapt.examples/gapt.examples.sequence/LinearEqExampleProof

LinearEqExampleProof

gapt.examples.sequence.LinearEqExampleProof
object LinearEqExampleProof extends TacticsProof, ProofSequence, ExplicitEqualityTactics

Functions to construct cut-free FOL LK proofs of the sequents

Refl, Trans, \ALL x. f(x) = x :- f^n^(a) = a

where n is an Integer parameter >= 0.

Attributes

Graph
Supertypes
class TacticsProof
class TacticsProof0
class Object
trait Matchable
class Any
Show all
Self type

Members list

Value members

Concrete methods

def apply(n: Int): LKProof

Inherited methods

def explicitRewriteLeft(equation: String, targetEq: String, transitivity: String): Tactic[Unit]

Applies the quantified equation ∀x(e_l=e_r) to the left side of the equation tgt_l=tgt_r, leaving open the subgoal e_r σ = tgt_r.

Applies the quantified equation ∀x(e_l=e_r) to the left side of the equation tgt_l=tgt_r, leaving open the subgoal e_r σ = tgt_r.

Attributes

Inherited from:
ExplicitEqualityTactics
def explicitRewriteRight(equation: String, targetEq: String, transitivity: String): Tactic[Unit]

Applies the quantified equation ∀x(e_l=e_r) to the right side of the equation tgt_l=tgt_r, leaving open the subgoal tgt_l = e_l σ.

Applies the quantified equation ∀x(e_l=e_r) to the right side of the equation tgt_l=tgt_r, leaving open the subgoal tgt_l = e_l σ.

Attributes

Inherited from:
ExplicitEqualityTactics
def main(args: Array[String]): Unit

Attributes

Inherited from:
TacticsProof
def name: String

Attributes

Inherited from:
ProofSequence

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

Inherited from:
TacticsProof0
Generated with