object Extensionality extends ExtensionalityRule with PiOrArrowRule
equality-checking: the extensionality rule (equivalent to Eta) x:A|-f x = g x : B ---> f = g : Pi x:A. B If possible, the name of the new variable x is taken from f, g, or their type; otherwise, a fresh variable is invented.
- Source
- Rules.scala
- Alphabetic
- By Inheritance
- Extensionality
- PiOrArrowRule
- ExtensionalityRule
- TypeBasedEqualityRule
- ApplicableUnder
- SingleTermBasedCheckingRule
- 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
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]
- Definition Classes
- PiOrArrowRule
-
def
applicable(tm: Term): Boolean
- Definition Classes
- ApplicableUnder → SingleTermBasedCheckingRule
-
def
applicableToTerm(solver: Solver, tm: Term): Boolean
type-based equality reasoning often uses extensionality, which can be inefficient or even lead to cycles.
type-based equality reasoning often uses extensionality, which can be inefficient or even lead to cycles. Therefore, these rules are only applied to tm1 = tm2 : tp if tm1 or tm2 satisfies this predicate.
- Definition Classes
- ExtensionalityRule → TypeBasedEqualityRule
-
def
apply(solver: Solver)(tm1: Term, tm2: Term, tp: Term)(implicit stack: Stack, history: History): Option[Boolean]
- 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
- Extensionality → TypeBasedEqualityRule
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
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
- TypeBasedEqualityRule → 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
-
val
introForm: Lambda.type
- Definition Classes
- Extensionality → ExtensionalityRule
-
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
-
val
under: List[GlobalName]
- Definition Classes
- TypeBasedEqualityRule → ApplicableUnder
-
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()