Package | Description |
---|---|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule.conditions | |
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.taclettranslation.assumptions |
Modifier and Type | Method and Description |
---|---|
static SortDependingFunction |
SortDependingFunction.createFirstInstance(GenericSort sortDependingOn,
Name kind,
Sort sort,
Sort[] argSorts,
boolean unique) |
Modifier and Type | Method and Description |
---|---|
GenericSort |
TypeResolver.GenericSortResolver.getGenericSort() |
Modifier and Type | Method and Description |
---|---|
static TypeResolver |
TypeResolver.createGenericSortResolver(GenericSort gs) |
Constructor and Description |
---|
FieldTypeToSortCondition(SchemaVariable exprOrTypeSV,
GenericSort sort) |
GenericSortResolver(GenericSort gs) |
JavaTypeToSortCondition(SchemaVariable exprOrTypeSV,
GenericSort sort,
boolean elemSort) |
Modifier and Type | Method and Description |
---|---|
GenericSort |
GenericSortCondition.getGenericSort() |
Modifier and Type | Method and Description |
---|---|
ImmutableMap<GenericSort,Sort> |
GenericSortInstantiations.getAllInstantiations()
ONLY FOR JUNIT TESTS
|
Modifier and Type | Method and Description |
---|---|
static GenericSortCondition |
GenericSortCondition.createForceInstantiationCondition(GenericSort p_gs,
boolean p_maximum) |
static GenericSortCondition |
GenericSortCondition.createIdentityCondition(GenericSort p_gs,
Sort p_s) |
static GenericSortCondition |
GenericSortCondition.createSupersortCondition(GenericSort p_gs,
Sort p_s) |
Sort |
GenericSortInstantiations.getInstantiation(GenericSort p_gs) |
boolean |
GenericSortInstantiations.isInstantiated(GenericSort p_gs) |
Modifier and Type | Method and Description |
---|---|
static GenericSortInstantiations |
GenericSortInstantiations.create(ImmutableList<GenericSort> p_sorts,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that holds instantiations of the generic sorts
"p_sorts" satisfying the conditions "p_conditions"
|
Constructor and Description |
---|
GenericSortCondition(GenericSort p_gs) |
Modifier and Type | Method and Description |
---|---|
static java.util.HashSet<GenericSort> |
AssumptionGenerator.collectGenerics(Term term) |
Modifier and Type | Method and Description |
---|---|
boolean |
DefaultTacletSetTranslation.eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term) |
boolean |
TranslationListener.eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term)
Called when the translator can not instantiate a generic sort
with a particular sort in the given term.
|
Copyright © 2003-2019 The KeY-Project.