public interface TacletFormula
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() |
Taclet getTaclet()
Term getFormula(TermServices services)
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.java.lang.String getStatus()
java.util.Collection<Term> getInstantiations()