object Solve extends ValueSolutionRule with ApplySolutionRule
solution: This rule tries to solve for an unknown by applying lambda-abstraction on both sides and eta-reduction on the left. Its effect is, for example, that X x = t is reduced to X = lambda x.t where X is a meta- and x an object variable.
- Source
- Rules.scala
- Alphabetic
- By Inheritance
- Solve
- ApplySolutionRule
- ValueSolutionRule
- SolutionRule
- CheckingRule
- SyntaxDrivenRule
- Rule
- SemanticObject
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
DelayJudgment(msg: String) extends Throwable with Product with Serializable
may be thrown to indicate that the judgment that the rules was called on should be delayed
may be thrown to indicate that the judgment that the rules was called on should be delayed
- Definition Classes
- CheckingRule
-
case class
Isolation(newContext: Context, bound: LocalName, boundTp: Term, rest: Term) extends Product with Serializable
- Attributes
- protected
- Definition Classes
- ApplySolutionRule
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
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
-
def
applicable(t: Term): Option[Int]
- returns
Some(i) if the rule is applicable to t1 in the judgment t1=t2, in that case, i is the position of the argument of t1 (starting from 0) that the rule will try to isolate this is about spotting unknowns, not predicting whether the isolation will succeed
- Definition Classes
- ApplySolutionRule → SolutionRule
-
def
apply(j: Equality): Option[(Equality, String)]
- j
the equality in which to isolate a variable on the left side
- returns
the transformed equality and a log message if a step towards isolation was possible
- Definition Classes
- Solve → ValueSolutionRule
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
bind(context: Context, tm: Term, other: Term): Option[Isolation]
returns Isolation(c, x, a, r) such that c, x:a |- tm = r x and x not occurring in c, r
returns Isolation(c, x, a, r) such that c, x:a |- tm = r x and x not occurring in c, r
- Attributes
- protected
- Definition Classes
- ApplySolutionRule
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
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
- ValueSolutionRule → SyntaxDrivenRule
-
def
heads: List[GlobalName]
- Definition Classes
- CheckingRule
-
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
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
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
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
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
-
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
-
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
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- SyntaxDrivenRule → Rule → AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()