Packages

final case class URename(what: Variable, repl: Variable, semantic: Boolean = false) extends (Expression) ⇒ Expression with Product with Serializable

Uniformly rename all occurrences of what and what' to repl and repl' and vice versa, but clash for program constants etc. Uniformly rename all occurrences of variable what (and its associated DifferentialSymbol what') to repl (and its associated DifferentialSymbol repl') everywhere and vice versa uniformly rename all occurrences of variable repl (and its associated DifferentialSymbol) to what (and what'). Uniform renaming, thus, is a transposition.

what

What variable to replace (along with its associated DifferentialSymbol).

repl

The target variable to replace what with and vice versa.

semantic

true to allow semantic renaming of SpaceDependent symbols, which preserves local soundness when applied to inferences.

Note

soundness-critical

See also

UniformRenaming

BoundRenaming

Provable.apply(ren:edu\.cmu\.cs\.ls\.keymaerax\.core\.URename):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

Linear Supertypes
Serializable, Serializable, Product, Equals, (Expression) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. URename
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. Function1
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new URename(what: Variable, repl: Variable, semantic: Boolean = false)

    what

    What variable to replace (along with its associated DifferentialSymbol).

    repl

    The target variable to replace what with and vice versa.

    semantic

    true to allow semantic renaming of SpaceDependent symbols, which preserves local soundness when applied to inferences.

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. def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  5. def apply(s: Sequent): Sequent

    Apply uniform renaming everywhere in the sequent.

    Apply uniform renaming everywhere in the sequent.

    Exceptions thrown

    RenamingClashException if this uniform renaming is not admissible for s (because a semantic symbol occurs despite !semantic).

  6. def apply(p: Program): Program

    apply this uniform renaming everywhere in a program.

    apply this uniform renaming everywhere in a program.

    Exceptions thrown

    RenamingClashException if this uniform renaming is not admissible for p (because a semantic symbol occurs despite !semantic).

  7. def apply(p: DifferentialProgram): DifferentialProgram

    apply this uniform renaming everywhere in a differential program.

    apply this uniform renaming everywhere in a differential program.

    Exceptions thrown

    RenamingClashException if this uniform renaming is not admissible for p (because a semantic symbol occurs despite !semantic).

  8. def apply(f: Formula): Formula

    apply this uniform renaming everywhere in a formula.

    apply this uniform renaming everywhere in a formula.

    Exceptions thrown

    RenamingClashException if this uniform renaming is not admissible for f (because a semantic symbol occurs despite !semantic).

  9. def apply(t: Term): Term

    apply this uniform renaming everywhere in a term.

    apply this uniform renaming everywhere in a term.

    Exceptions thrown

    RenamingClashException if this uniform renaming is not admissible for t (because a semantic symbol occurs despite !semantic).

  10. def apply(e: Expression): Expression

    apply this uniform renaming everywhere in an expression, resulting in an expression of the same kind.

    apply this uniform renaming everywhere in an expression, resulting in an expression of the same kind.

    Definition Classes
    URename → Function1
  11. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  12. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  13. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  16. final def getClass(): Class[_]
    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(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. val repl: Variable
  22. val semantic: Boolean
  23. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  24. def toString(): String
    Definition Classes
    URename → Function1 → AnyRef → Any
  25. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  28. val what: Variable

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped