simp_expr_unambig1

gapt.examples.tip.grammars.simp_expr_unambig1
object simp_expr_unambig1 extends TacticsProof

Attributes

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

Members list

Value members

Inherited methods

def main(args: Array[String]): Unit

Attributes

Inherited from:
TacticsProof

Concrete fields

val app_assoc: Formula
val cong_neg: Sequent[(String, Formula)]
val cong_neg_proof: LKProof
val cong_neg_symm: Sequent[(String, Formula)]
val cong_neg_symm_proof: LKProof
val cong_pos: Sequent[(String, Formula)]
val cong_pos_proof: LKProof
val lem: Formula
val lem_proof: LKProof
val proof: LKProof
val sequent: Sequent[(String, Formula)]
val theory: Sequent[(String, Formula)]

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

Inherited from:
TacticsProof0