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

SumOfOnesFExampleProof

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

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