Packages

sealed trait Position extends AnyRef

Position at which formula and subexpresion ofa a sequent to apply a tactic.

To do

use AntePos and SuccPos directly instead of index etc.

Position should essentially become a nice type-preserving name for a pair of a SeqPos and a PosInExpr.

See also

edu.cmu.cs.ls.keymaerax.core.SeqPos

Linear Supertypes
AnyRef, Any
Known Subclasses
AntePosition, SuccPosition, TopAntePosition, TopPosition, TopSuccPosition
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Position
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def ++(child: PosInExpr): Position

    Append child to obtain position of given subexpression by concatenating p2 to this.

  2. abstract def advanceIndex(i: Int): Position

    Advances the index by i on top-level, does not affect inExpr.

  3. abstract def checkAnte: AntePosition

    This position if it is an AntePosition, otherwise an error (convenience)

  4. abstract def checkSucc: SuccPosition

    This position if it is a SuccPosition, otherwise an error (convenience)

  5. abstract def inExpr: PosInExpr

    The subexpression position within the formula

  6. abstract def top: SeqPos

    The top-level part of this position

  7. abstract def topLevel: TopPosition

    Top level position of this position

    Top level position of this position

    returns

    A position with the same index but on the top level (i.e., inExpr == HereP)

  8. abstract def navigate(instead: PosInExpr): Position

    Return a position with inExpr replaced by p

    Return a position with inExpr replaced by p

    Annotations
    @deprecated
    Deprecated

    Unsure whether this will be kept

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 checkTop: SeqPos

    The top-level part of this position provided this position isTop (convenience)

  6. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def isAnte: Boolean

    Whether this position is in the antecedent on the left of the sequent arrow

  13. def isIndexDefined(s: Sequent): Boolean

    Check whether top-level index of this position is defined in given sequent (ignoring inExpr).

  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. def isSucc: Boolean

    Whether this position is in the succedent on the right of the sequent arrow

  16. def isTopLevel: Boolean

    Whether this position is a top-level position of a sequent instead of a subexpression.

  17. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  19. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. def parent: Option[Position]

    The parent of this position (None if this is a top-level position)

  21. def prettyString: String
  22. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  23. def toString(): String
    Definition Classes
    Position → 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( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped