Packages

object KaisarProof

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

Type Members

  1. case class ElaborationException(msg: String, node: ASTNode = Triv()) extends NodeException with Product with Serializable
  2. type Ident = Variable
  3. type IdentPat = Term
  4. case class KaisarParseException(msg: String = "", trace: Option[TracedFailure] = None, location: Option[Int], source: String) extends LocatedException with Product with Serializable
  5. case class LabelDef(label: TimeIdent, args: List[Variable] = Nil) extends Product with Serializable
  6. case class LabelRef(label: TimeIdent, args: List[Term] = Nil) extends Product with Serializable
  7. abstract class LocatedException extends Exception
  8. class NodeException extends LocatedException
  9. case class ODEAdmissibilityException(vars: Set[Variable], node: ASTNode = Triv()) extends NodeException with Product with Serializable
  10. case class ProofCheckException(msg: String, cause: Throwable = null, node: ASTNode = Triv()) extends NodeException with Product with Serializable
  11. type Statements = List[Statement]
  12. type Subscript = Option[Int]
  13. type TimeIdent = String
  14. case class TransformationException(msg: String, node: ASTNode = Triv()) extends NodeException with Product with Serializable

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. val abs: Function
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. val askLaterP: PredOf
  7. val askLaterPF: Function
  8. val askLaterT: FuncOf
  9. val askLaterTF: Function

    askLaterT is strictly used in the internal representation.

    askLaterT is strictly used in the internal representation. If a term cannot be elaborated until a later proof-checking pass, then symbol askLaterT is used to represent a dummy term

  10. val at: Function
  11. def block(ss: Statements): Statement
  12. val builtin: Set[Function]
  13. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  16. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  17. def flatten(ss: Statements): Statements
  18. def forgetAt(e: Formula): Formula
  19. def forgetAt(e: Term): Term
  20. def getAt(t: Formula, node: ASTNode): Option[(Formula, LabelRef)]
  21. def getAt(t: Term, node: ASTNode = Triv()): Option[(Term, LabelRef)]
  22. def getBuiltin(f: String): Option[Function]
  23. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  24. def getStable(t: Term): Option[Term]
  25. def ghost(s: Statement): Statement
  26. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  27. val init: FuncOf
  28. def inverseGhost(s: Statement): Statement
  29. def isBuiltinFunction(f: Function): Boolean
  30. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  31. def makeAt(f: Formula, lr: LabelRef): Formula
  32. def makeAt(f: Term, lr: LabelRef): Term
  33. val max: Function
  34. val min: Function
  35. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  36. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  37. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  38. val stable: Function
  39. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  40. def toString(): String
    Definition Classes
    AnyRef → Any
  41. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  42. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  43. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  44. val wild: FuncOf
  45. object IdentPat

Inherited from AnyRef

Inherited from Any

Ungrouped