add final type to mgu in LatexCreator

This commit is contained in:
ucrhh 2021-02-09 22:19:22 +01:00
parent 363646f6d2
commit 34a727e0c0

View File

@ -55,8 +55,10 @@ public class LatexCreatorConstraints implements StepVisitor {
typeInferer.getMGU().ifPresent(mgu -> { typeInferer.getMGU().ifPresent(mgu -> {
result.add(generateMGU()); result.add(generateMGU());
numberGenerator.push(); numberGenerator.push();
result.add(generateMGU() + LATEX_NEW_LINE + new LatexCreatorType(typeInferer.getType().get()).getLatex());
numberGenerator.push();
}); });
// todo return final type, dont forget numberGenerator.push(); // todo add some helpful text for the user
if (FIRST_PREFIX.equals(prefix)) { if (FIRST_PREFIX.equals(prefix)) {
result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END); result.replaceAll(content -> ALIGN_BEGIN + content + ALIGN_END);
} }