t

# Expression 

#### sealed trait Expression extends AnyRef

Expressions of differential dynamic logic. Expressions are categorized according to the syntactic categories of the grammar of differential dynamic logic:

1. terms are of type edu.cmu.cs.ls.keymaerax.core.Term of kind edu.cmu.cs.ls.keymaerax.core.TermKind

See Section 2.1

DifferentialProgram

Program

Formula

Term

Syntax of differential dynamic logic

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser#apply

Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.

Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

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

### Abstract Value Members

1. abstract val kind: Kind

What kind of an expression this is, e.g., TermKind, FormulaKind, ProgramKind.

2. abstract val sort: Sort

The sort of this expression, e.g., Real, Bool.

### 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(): scala.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. final def isInstanceOf[T0]: Boolean
Definition Classes
Any
12. final def ne(arg0: AnyRef): Boolean
Definition Classes
AnyRef
13. final def notify(): scala.Unit
Definition Classes
AnyRef
Annotations
@native()
14. final def notifyAll(): scala.Unit
Definition Classes
AnyRef
Annotations
@native()
15. def prettyString: String

Pretty-printed string representing this expression

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