Packages

t

info.kwarc.mmt.api.checking

CheckingCallback

trait CheckingCallback extends AnyRef

passed to Rules to permit callbacks to the Solver

Source
Rules.scala
Linear Supertypes
AnyRef, Any
Known Subclasses
Solver
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. CheckingCallback
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def check(j: Judgement)(implicit history: History): Boolean

    checking

  2. abstract def lookup: Lookup

    lookup

  3. abstract def outerContext: Context

    a fixed context prefix that is not part of the contexts passed to the other methods

  4. abstract def simplify(t: Obj)(implicit stack: Stack, history: History): ThisType

    type inference, fails by default

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[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  6. def dryRun[A](allowDelay: Boolean, commitOnSuccess: (A) ⇒ Boolean)(code: ⇒ A): DryRunResult

    runs code and succeeds by default

  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def error(message: ⇒ String)(implicit history: History): Boolean

    flag an error

  10. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def inferType(t: Term, covered: Boolean = false)(implicit stack: Stack, history: History): Option[Term]
  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. def safeSimplifyUntil[A](tm: Term)(simple: (Term) ⇒ Option[A])(implicit stack: Stack, history: History): (Term, Option[A])
  19. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  20. def toString(): String
    Definition Classes
    AnyRef → Any
  21. def tryToCheckWithoutDelay(js: Judgement*): Option[Boolean]

    tries to check some judgments without delaying constraints

    tries to check some judgments without delaying constraints

    if this returns None, the check is inconclusive at this point, and no state changes were applied if this returns Some(true), all judgments have been derived and all state changes are applied if this returns Some(false), no state changes are applied and the caller still has to generate an error message, possibly by calling check(j)

  22. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  23. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  24. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from AnyRef

Inherited from Any

Ungrouped