Packages

sealed trait RenUSubst extends (Expression) ⇒ Expression

Renaming Uniform Substitution, combining URename and USubst in a way that has both a direct application like apply functions of USubstRen as well as a translation to equivalent tactical/core prover operations.

Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution.

See also

edu.cmu.cs.ls.keymaerax.core.URename

edu.cmu.cs.ls.keymaerax.core.USubst

USubstRen

edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()

edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()

edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

Linear Supertypes
(Expression) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. RenUSubst
  2. Function1
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type RenUSubstRepl = (Expression, Expression)

    A renaming substitution pair for a renaming uniform substitution.

    A renaming substitution pair for a renaming uniform substitution.

    See also

    edu.cmu.cs.ls.keymaerax.core.SubstitutionPair

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

Abstract Value Members

  1. abstract def apply(p: DifferentialProgram): DifferentialProgram
  2. abstract def apply(p: Program): Program
  3. abstract def apply(f: Formula): Formula
  4. abstract def apply(t: Term): Term
  5. abstract def getRenamingTactic: BelleExpr

    Get the renaming tactic part that performs this renaming

  6. abstract def renaming: RenUSubst

    The uniform renaming part of this renaming uniform substitution

  7. abstract def substitution: RenUSubst

    The uniform substitution part of this renaming uniform substitution as a RenUSubst

    The uniform substitution part of this renaming uniform substitution as a RenUSubst

    See also

    usubst

  8. abstract def toCore: (Expression) ⇒ Expression

    This RenUSubst implemented strictly from the core.

    This RenUSubst implemented strictly from the core.

    Note

    For contract purposes

  9. abstract def toForward: (ProvableSig) ⇒ ProvableSig

    Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.

  10. abstract def usubst: USubst

    The uniform substitution part of this renaming uniform substitution as a USubst

    The uniform substitution part of this renaming uniform substitution as a USubst

    See also

    substitution

Concrete Value Members

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

    Union of renaming uniform substitutions, i.e., both replacement lists merged.

  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  6. def apply(s: Sequent): Sequent

    Apply everywhere in the sequent.

  7. def apply(e: Expression): Expression
    Definition Classes
    RenUSubst → Function1
  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  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 hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def isEmpty: Boolean

    Returns true if there is no replacement.

  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. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  22. def toString(): String
    Definition Classes
    Function1 → AnyRef → Any
  23. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  24. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  25. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped