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 alternativeHeads: List[GlobalName]

   additional heads that can trigger the rule, e.g., arrow for a rule with head Pi

   additional heads that can trigger the rule, e.g., arrow for a rule with head Pi

   Definition Classes

   CheckingRule

5.  def applicable(tm: Term): Boolean

   Definition Classes

   ApplicableUnder → SingleTermBasedCheckingRule

6.  def applicableToTerm(solver: Solver, tm: Term): Boolean

   always true as the shape of terms is irrelevant anyway

   always true as the shape of terms is irrelevant anyway

   Definition Classes

   TypeBasedSolutionRule → TypeBasedEqualityRule

7.  def apply(solver: Solver)(tm1: Term, tm2: Term, tp: Term)(implicit stack: Stack, history: History): Option[Boolean]

   always true

   always true

   solver

   provides callbacks to the currently solved system of judgments

   tm1

   the first term

   tm2

   the second term

   tp

   their type

   stack

   their context

   returns

   true iff the judgment holds; None if the solver should proceed with term-based equality checking

   Definition Classes

   SimpleIrrelevanceRule → TypeBasedSolutionRule → TypeBasedEqualityRule

8.  final def asInstanceOf[T0]: T0

   Definition Classes

   Any

9.  def clone(): AnyRef

   Attributes

   protected[lang]

   Definition Classes

   AnyRef

   Annotations

   @throws( ... ) @native()

10.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

11.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

12.  def finalize(): Unit

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

13.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

14.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

15.  val head: GlobalName

    an MMT URI that is used to indicate when the Rule is applicable

    an MMT URI that is used to indicate when the Rule is applicable

    Definition Classes

    TypeBasedEqualityRule → SyntaxDrivenRule

16.  def heads: List[GlobalName]

    Definition Classes

    CheckingRule

17.  def init: Unit

    errors in Java initializers are hard to debug; therefore, objects should put initialization code here, which will be called by MMT empty by default, may throw errors

    errors in Java initializers are hard to debug; therefore, objects should put initialization code here, which will be called by MMT empty by default, may throw errors

    Definition Classes

    SemanticObject

18.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

19.  lazy val mpath: MPath

    the MMT URI of this object, derived from its Scala name: scala://package?name

    the MMT URI of this object, derived from its Scala name: scala://package?name

    Definition Classes

    SemanticObject

20.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

21.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

22.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

23.  def priority: Int

    when multiple rules are applicable, rules with higher priorities are preferred

    when multiple rules are applicable, rules with higher priorities are preferred

    creating a new rule with higher priority can be used to effectively drop imported rules

    Definition Classes

    Rule

24.  def providedRules: List[Rule]

    normally the singleton list of this rule; but rules may bundle additional rules as well

    normally the singleton list of this rule; but rules may bundle additional rules as well

    Definition Classes

    Rule

25.  def shadowedRules: List[Rule]

    normally the empty list; but rules may list rules here that should be removed from the context this can be used to override imported rules

    normally the empty list; but rules may list rules here that should be removed from the context this can be used to override imported rules

    Definition Classes

    Rule

26.  def solve(solver: Solver)(tp: Term)(implicit stack: Stack, history: History): Option[Term]

    if this type is proof-irrelevant, this returns the unique term of this type

    if this type is proof-irrelevant, this returns the unique term of this type

    This method is already called during equality-checking. Therefore, it may not perform complex search operations.

    Definition Classes

    SimpleIrrelevanceRule → TypeBasedSolutionRule

27.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

28.  def toString(): String

    Definition Classes

    SyntaxDrivenRule → Rule → AnyRef → Any

29.  val under: List[GlobalName]

    Definition Classes

    TypeBasedEqualityRule → ApplicableUnder

30.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

31.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

32.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()