gapt-examples
API
Generated with
gapt-examples/gapt.examples/ringinv

ringinv

gapt.examples.ringinv
object ringinv extends TacticsProof

Attributes

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

Members list

Value members

Concrete methods

def proof_acnf: LKProof

Inherited methods

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

Attributes

Inherited from:
TacticsProof

Concrete fields

val absorption0Left: LKProof
val absorption0Right: LKProof
val axioms: Sequent[(String, Formula)]
val cancellationPlus: LKProof
val multClosed_Inv: LKProof
val multMinusLeft: LKProof
val multMinusRight: LKProof
val multleftCompatibility: LKProof
val multleftDistributive: LKProof
val multleftSubset: LKProof
val multsetAssoc: LKProof
val plusClosed: LKProof
val proof: LKProof
val setMult1_Equal: LKProof
val setMultClosed: LKProof
val setPlusClosed: LKProof
val setPlusSubset: LKProof
val subAntisymmetry: LKProof
val subReflexivity: LKProof
val subTransitivity: LKProof
val sumCompatibility: LKProof

Implicits

Inherited implicits

implicit def ctx: ImmutableContext

Attributes

Inherited from:
TacticsProof0
Generated with