public class AssumptionFormula extends java.lang.Object implements TacletFormula
Modifier and Type | Field and Description |
---|---|
(package private) TacletConditions |
conditions |
(package private) java.util.Collection<Term> |
formula |
(package private) java.lang.String |
status |
(package private) Taclet |
taclet |
Constructor and Description |
---|
AssumptionFormula(Taclet taclet,
java.util.Collection<Term> formula,
java.lang.String status) |
AssumptionFormula(Taclet taclet,
java.util.Collection<Term> formula,
java.lang.String status,
TacletConditions conditions) |
Modifier and Type | Method and Description |
---|---|
TacletConditions |
getConditions() |
Term |
getFormula(TermServices services) |
java.util.Collection<Term> |
getInstantiations()
It can be that a taclet is translated into several formulas, i.e. in the case
that the generics are instantiated.
|
java.lang.String |
getStatus() |
Taclet |
getTaclet() |
Taclet taclet
java.util.Collection<Term> formula
java.lang.String status
TacletConditions conditions
public AssumptionFormula(Taclet taclet, java.util.Collection<Term> formula, java.lang.String status)
public AssumptionFormula(Taclet taclet, java.util.Collection<Term> formula, java.lang.String status, TacletConditions conditions) throws IllegalTacletException
IllegalTacletException
public TacletConditions getConditions()
public Term getFormula(TermServices services)
getFormula
in interface TacletFormula
services
- TODOnull
. If the translation of the taclet
consists of several instantiations (e.g. the taclet has some
generic sorts) the returned term is a conjunction of these
instantiations.public Taclet getTaclet()
getTaclet
in interface TacletFormula
public java.lang.String getStatus()
getStatus
in interface TacletFormula
public java.util.Collection<Term> getInstantiations()
TacletFormula
getInstantiations
in interface TacletFormula