diff --git a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java
index ae9c3c2..4912b06 100644
--- a/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java
+++ b/src/main/java/edu/kit/typicalc/view/main/HelpDialog.java
@@ -83,6 +83,7 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
acc.add(new HelpContentField("root.typeInferButton", "root.helpTypeInferButton"));
acc.add(new HelpContentField("root.inputField", "root.helpInputField"));
acc.add(new HelpContentField("root.typeAssumptions", "root.helpTypeAssumptions"));
+ acc.add(new HelpContentField("root.inferenceViewFeatures", "root.helpInferenceViewFeatures"));
acc.add(new HelpContentField("root.shortcuts", shortcuts));
acc.add(new HelpContentField("root.drawer",
new Button(new Icon(VaadinIcon.MENU)), "root.helpDrawer"));
diff --git a/src/main/resources/language/translation_de.properties b/src/main/resources/language/translation_de.properties
index 49938ec..cb16da0 100644
--- a/src/main/resources/language/translation_de.properties
+++ b/src/main/resources/language/translation_de.properties
@@ -34,6 +34,7 @@ root.previousStepButton=Vorheriger-Schritt-Knopf
root.nextStepButton=Nächster-Schritt-Knopf
root.lastStepButton=Letzter-Schritt-Knopf
root.shareButton=Teilen-Knopf
+root.inferenceViewFeatures=Typherleitungsbaum und Unifikation
root.helpDrawer=Durch Benutzen des Knopfs öffnet sich der Drawer. \
Im Drawer ist eine Auflistung aller Typinferenzregeln zu finden. \
Außerdem kann mit dem Kopieren-Knopf der Latex-Code der Regel in die Zwischenablage kopiert werden.
@@ -75,8 +76,15 @@ root.helpShareButton=Durch Benutzen des Teilen-Knopfs öffnet sich ein Dialog, i
Typherleitungsbaums des eingegebenen Terms und die benötigen Pakete zum Einbinden des LaTeX-Codes angezeigt werden. \
Zusätzlich dazu enthält der Dialog einen Permalink zur aktuellen Seite, der sowohl den Term als auch die Typannahmen \
kodiert.
+root.helpInferenceViewFeatures=Wurde ein Term erfolgreich typisiert, werden der Typherleitungsbaum und die \
+ Unifikation angezeigt. Der Baum lässt sich durch Scrollen mit der Maus vergrößern und verkleinern und durch Halten \
+ und Ziehen mit der linken Maustaste verschieben. Die Constraints bauen sich parallel zum Baum im Feld darüber auf. \
+ Bei der Unifikation werden dann die sich verändernden Stellen in den Constraints in jedem Schritt farblich \
+ hervorgehoben. Kommt im eingegebenen Term let-Polymorphismus vor, wird im Constraint-Feld zunächst \
+ die Unifikation der Constraints vom let-Teilbaum durchgeführt, bevor der Baum weiter aufgebaut wird. \
+ Mit \u03C3 wird am Ende der allgemeinste Unifikator angegeben, mit \u03C3(\u03B1\u2081) der finale Typ des Terms.
help.typicalcInfo=\
-Typicalc wurde als PSE-Projekt am KIT im WS20/21 entwickekt von
\
+Typicalc wurde als PSE-Projekt am KIT im WS20/21 entwickelt von
\
Robin Böhne
\
Moritz Dieing
\
Thomas Heinen
\
diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties
index 9c96375..1746c80 100644
--- a/src/main/resources/language/translation_en.properties
+++ b/src/main/resources/language/translation_en.properties
@@ -34,6 +34,7 @@ root.previousStepButton=Previous-Step Button
root.nextStepButton=Next-Step Button
root.lastStepButton=Last-Step Button
root.shareButton=Share Button
+root.inferenceViewFeatures=Inference Tree And Unification
root.helpDrawer=Clicking on the button opens up the drawer. The drawer contains a collection of all type inference \
rules. By clicking on the copy button the LaTeX code of the corresponding rule is copied to the clipboard.
root.helpExample=Clicking on the button opens up the example dialog. After clicking on an example the corresponding \
@@ -49,7 +50,7 @@ the algorithm. If the type of a type assumptions starts with a 't' followed by o
converted to a type variable.
root.helpTypeInferButton=Clicking on the type button starts the type inference algorithm for the current input. \
The longer the entered term the longer the time to display the type inference tree. With a slow computer or a \
-very long term a lot of patience will be required.
+very long term some patience will be required.
root.helpShortcuts=Ctrl + \u2190 = First step
\
\u2190 = Previous step
\
\u2192 = Next step
\
@@ -70,6 +71,13 @@ entered term. The key combination "CTRL + right arrow key" also executes a click
root.helpShareButton=Clicking the share button opens up a dialog containing the LaTeX code of the final inference \
tree and the packages needed to compile the LaTeX code. In addition a permalink to the current page is provided. \
This link encodes the current term as well as the current type assumptions.
+root.helpInferenceViewFeatures=When a term is successfully type inferred, the inference tree and the unification are \
+ displayed. To zoom in and out the inference tree, scroll with your mouse. To move the tree, drag it with your \
+ pressed left mouse button. While the tree is building up, the resulting constraints build up simultaneously in the \
+ field above. During the unification, the modified constraints are then highlighted in each step. \
+ If the entered term contains let polymorphism, the constraints of the let sub-tree are unified before further \
+ steps in the tree are shown. At the end, the most general unifier is displayed as \u03C3 and the final type \
+ as \u03C3(\u03B1\u2081).
help.typicalcInfo=\
Typicalc was developed as a PSE project at the KIT in WS20/21 by
\
Robin Böhne
\