Packages

c

edu.cmu.cs.ls.keymaerax.pt

RuleApplication

case class RuleApplication(child: ProofTerm, rule: Rule, subgoal: Int) extends ProofTerm with Product with Serializable

Witness for rule application.

Linear Supertypes
Serializable, Serializable, Product, Equals, ProofTerm, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. RuleApplication
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. ProofTerm
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new RuleApplication(child: ProofTerm, rule: Rule, subgoal: Int)

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val args: List[Expression]
  5. def arithmeticGoals: Set[Formula]
    Definition Classes
    ProofTerm
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def axiomsUsed: Set[String]
    Definition Classes
    ProofTerm
  8. def bytesEstimate: Int
    Definition Classes
    ProofTerm
  9. val child: ProofTerm
  10. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def equals(other: Any): Boolean
    Definition Classes
    ProofTerm → AnyRef → Any
  13. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  17. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  19. def numCons: Int
    Definition Classes
    ProofTerm
  20. val positions: List[SeqPos]
  21. def prettyString: String
    Definition Classes
    ProofTerm
  22. val rule: Rule
  23. def rulesUsed: Set[String]
    Definition Classes
    ProofTerm
  24. val subgoal: Int
  25. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  26. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  29. val wordSize: Int
    Definition Classes
    ProofTerm

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from ProofTerm

Inherited from AnyRef

Inherited from Any

Ungrouped