class SimpleIrrelevanceRule extends TypeBasedSolutionRule
Irrelevance rules for (usually atomic) types that introduce proof irrelevance (as opposed to complex that happen to be irrelevant because their components are): - terms of these types are always equal - unknowns terms of these types are found using proof search; if provided, a default value is used to recover if search fails
- Alphabetic
- By Inheritance
- SimpleIrrelevanceRule
- TypeBasedSolutionRule
- TypeBasedEqualityRule
- ApplicableUnder
- SingleTermBasedCheckingRule
- CheckingRule
- SyntaxDrivenRule
- Rule
- SemanticObject
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new SimpleIrrelevanceRule(p: GlobalName, default: Option[Term] = None)
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]
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(tm: Term): Boolean
- Definition Classes
- ApplicableUnder → SingleTermBasedCheckingRule
-
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
-
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
-
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
-
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
-
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
-
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()