gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.examples/gapt.examples.sequence/ExplicitEqualityTactics

ExplicitEqualityTactics

gapt.examples.sequence.ExplicitEqualityTactics
trait ExplicitEqualityTactics

Attributes

Source
ExplicitEqualityTactics.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Known subtypes
object LinearEqExampleProof.type

Members list

Value members

Concrete 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

Source
ExplicitEqualityTactics.scala
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

Source
ExplicitEqualityTactics.scala
Generated with