Skip to content
Snippets Groups Projects
Commit 9c2d2694 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add comments about WD export of theory operators


cf issue #325

Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent a816ffee
No related branches found
No related tags found
No related merge requests found
Pipeline #121222 passed
...@@ -322,7 +322,7 @@ public class Theories { ...@@ -322,7 +322,7 @@ public class Theories {
throws CoreException { throws CoreException {
prologOutput.openTerm("operator"); prologOutput.openTerm("operator");
prologOutput.printAtom(opDef.getLabel()); prologOutput.printAtom(opDef.getLabel()); // Name of the operator
final FormulaFactory ff = theory.getFormulaFactory(); final FormulaFactory ff = theory.getFormulaFactory();
final ITypeEnvironment teFromFF = theory.getTypeEnvironment(ff); final ITypeEnvironment teFromFF = theory.getTypeEnvironment(ff);
...@@ -337,6 +337,9 @@ public class Theories { ...@@ -337,6 +337,9 @@ public class Theories {
} }
// WD Condition // WD Condition
// TODO: does not seem to get the user-defined WD conditions
// we should probably call in INewOperatorDefinition.java : IOperatorWDCondition[] getOperatorWDConditions() throws RodinDBException;
// and convert this to a Predicate
Predicate wdCondition = opDef.getWDCondition(ff, te); Predicate wdCondition = opDef.getWDCondition(ff, te);
printPredicate(prologOutput, wdCondition); printPredicate(prologOutput, wdCondition);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment