Packages

abstract class BelleExpr extends AnyRef

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. BelleExpr
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new BelleExpr(location: Location = UnknownLocation)

Abstract Value Members

  1. abstract def prettyString: String

    pretty-printed form of this Bellerophon tactic expression

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def &(other: BelleExpr): SeqTactic

    this & other: sequential composition this ; other executes other on the output of this, failing if either fail.

  4. def *(n: Int): RepeatTactic

    this*n: bounded repetition executes this tactic to times number of times, failing if any of those repetitions fail.

  5. def <(children: BelleExpr*): SeqTactic

    <(e1,...,en): branching to run tactic ei on branch i, failing if any of them fail or if there are not exactly n branches.

    <(e1,...,en): branching to run tactic ei on branch i, failing if any of them fail or if there are not exactly n branches.

    Note

    Equivalent to

    a & Idioms.<(b,c)
  6. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  7. def >(other: BelleExpr): AfterTactic

    this > other: followup composition executes other on the output or error of this, failing if other fails.

  8. def U(p: (SequentType, (RenUSubst) ⇒ BelleExpr)*): SeqTactic

    case _ of {fi => ei} uniform substitution case pattern applies the first ei such that fi uniformly substitutes to current provable for which ei does not fail, fails if the ei of all matching fi fail.

  9. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  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(arg0: Any): Boolean
    Definition Classes
    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. def getLocation: Location
  16. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. def setLocation(newLocation: Location): Unit

    Note

    location is private so that it's not something that effects case class quality, and mutable so that it can be ignored when building up custom tactics.

  22. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  23. def toString(): String
    Definition Classes
    BelleExpr → AnyRef → Any
  24. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  25. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  27. def |(other: BelleExpr): EitherTactic

    this | other: alternative composition executes other if applying this fails, failing if both fail.

Deprecated Value Members

  1. def *: SaturateTactic

    (this*): saturating repetition executes this tactic to a fixpoint, casting result to type annotation, diverging if no fixpoint.

    (this*): saturating repetition executes this tactic to a fixpoint, casting result to type annotation, diverging if no fixpoint.

    Annotations
    @deprecated
    Deprecated

    Use SaturateTactic(this) instead to avoid postfix parse

  2. def partial: PartialTactic

    partial: marks a tactic that is allowed to not close all its goals.

    partial: marks a tactic that is allowed to not close all its goals.

    Annotations
    @deprecated
    Deprecated

    Only useful in unit tests

Inherited from AnyRef

Inherited from Any

Ungrouped