class LemmaFormula extends java.lang.Object implements TacletFormula
Modifier and Type | Field and Description |
---|---|
private java.util.LinkedList<Term> |
formula |
private Taclet |
taclet |
Constructor and Description |
---|
LemmaFormula(Taclet taclet,
Term formula) |
Modifier and Type | Method and Description |
---|---|
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() |
public Taclet getTaclet()
getTaclet
in interface TacletFormula
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 java.lang.String getStatus()
getStatus
in interface TacletFormula
public java.util.Collection<Term> getInstantiations()
TacletFormula
getInstantiations
in interface TacletFormula