Packages

sealed trait DerivationInfo extends AnyRef

Meta-information on a derivation step, which is an axiom, derived axiom, proof rule, or tactic.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DerivationInfo
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def belleExpr: Any

    Bellerophon tactic implementing the derivation.

    Bellerophon tactic implementing the derivation. For non-input tactics this is simply a BelleExpr. For input tactics it is (curried) function which accepts the inputs and produces a BelleExpr.

  2. abstract val canonicalName: String

    Canonical name unique across all derivations (axioms or tactics).

    Canonical name unique across all derivations (axioms or tactics). For axioms this is as declared in the axioms file, for and tactics it is identical to codeName. Can and will contain spaces and special chars.

  3. abstract val codeName: String

    The unique alphanumeric identifier for this inference step.

  4. abstract val display: DisplayInfo

    How to display this inference step in a UI

Concrete 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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  7. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  8. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  9. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  10. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. val inputs: List[ArgInfo]

    Specification of inputs (other than positions) to the derivation, along with names to use when displaying in the UI.

  12. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  13. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. val needsGenerator: Boolean

    Whether the derivation expects the caller to provide it with a way to generate invariants

  15. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  16. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. val numPositionArgs: Int

    Number of positional arguments to the derivation.

    Number of positional arguments to the derivation. Can be 0, 1 or 2.

  18. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  19. def toString(): String
    Definition Classes
    DerivationInfo → AnyRef → Any
  20. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  21. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  22. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped