| java.lang.Object de.uka.ilkd.key.logic.MetavariableDeliverer
MetavariableDeliverer | public class MetavariableDeliverer (Code) | | |
MetavariableDeliverer | public MetavariableDeliverer(Proof p_proof)(Code) | | |
createNewMatchVariable | public static Metavariable createNewMatchVariable(String p_basename, Sort p_sort, Services services)(Code) | | Create new variable for instantiation of unknown schema
variables when applying taclets.
Parameters: p_sort - Sort of the variable New metavariable, or null iff p_sort allows nometavariables |
createNewVariable | public Metavariable createNewVariable(String name, Sort p_sort)(Code) | | Create new metavariable and add it to the namespace var_ns of
the mediator.
Parameters: name - name of the variable Parameters: p_sort - Sort of the variable New metavariable, or null iff p_sort allows nometavariables |
mv_Counter | public static int mv_Counter(String base, Goal g)(Code) | | Construct a unique identifier by adding a number to the base
name
|
|
|