mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
typos in operating help, add let example from Übungsblatt
This commit is contained in:
parent
13c746a0b1
commit
8ca72a77e2
@ -22,7 +22,8 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
|
||||
private static final String EXAMPLE_DIALOG_ID = "exampleDialog";
|
||||
|
||||
private static final List<String> EXAMPLES =
|
||||
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)",
|
||||
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "let k = λx.λy. x in k a (k b c)",
|
||||
"(λx.x x) (λx.x x)",
|
||||
"(λx.λy.y (x y)) (λz. λa. z g a)", "let f = λx. let g = λy. y in g x in f 3",
|
||||
"let f = λx. let g = λy.5 5 in g x in f 3");
|
||||
private final H3 instruction;
|
||||
|
@ -36,7 +36,7 @@ Im Drawer ist eine Auflistung aller Typregeln zu finden. \
|
||||
Außerdem kann durch Klicken des Kopieren-Knopfs der Latex-Code der Regel in die Zwischenablage kopiert werden.
|
||||
root.helpExample=Durch Klicken des Knopfs öffnet sich der Beispiel-Dialog. \
|
||||
Nach Anklicken wird der jeweilige Beispielterm in das Eingabefeld eingefügt. \
|
||||
Der Term kann nun nach belieben angepasst oder direkt typisiert werden.
|
||||
Der Term kann nun nach Belieben angepasst oder direkt typisiert werden.
|
||||
root.helpInputField=In das Eingabefeld können Lambda-Terme mit einer Länge von bis zu 1000 Zeichen eingegeben werden. \
|
||||
Das \u03BB-Zeichen kann dabei entweder durch Klicken des \u03BB-Knopfs oder durch Eingabe eines Backslashs an der \
|
||||
aktuellen Cursorposition eingefügt werden. Durch Klicken des Info-Symbols wird die korrekte Syntax eines Terms \
|
||||
@ -45,7 +45,7 @@ root.helpTypeAssumptions=Durch Klicken des Typannahmen-Knopfs öffnet sich ein D
|
||||
Durch Klicken des Info-Symbols wird die korrekte Syntax des Typs einer Typannahme angezeigt. Sofern eine Variable in \
|
||||
mehreren Typannahmen vorkommt, wird ausschließlich die oberste Typannahme, die diese Variable enthält, \
|
||||
berücksichtigt.
|
||||
root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funtion des Knopfs. \
|
||||
root.helpFirstStepButton=Je nach Stand der Algorithmusausführung ändert sich die FunKtion des Knopfs. \
|
||||
Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Klicken des Knopfs zurück zum ersten Schritt des \
|
||||
Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Klicken des Knopfs \
|
||||
in den letzten Schritt des Baums. Der Knopf lässt sich außerdem durch die Tastenkombination "STRG + Linke Pfeiltaste" \
|
||||
@ -54,13 +54,13 @@ root.helpPreviousStepButton=Durch Klicken des Vorheriger-Schritt Knopfs wird der
|
||||
angezeigt. Der Knopf lässt sich außerdem auf der Tastatur durch die Taste "Linke Pfeiltaste" ansprechen.
|
||||
root.helpNextStepButton=Durch Klicken des Nächster-Schritt Knopfs wird der nächste Schritt des Algorithmus angezeigt. \
|
||||
Der Knopf lässt sich außerdem durch auf der Tastatur durch die Taste "Rechte Pfeiltaste" ansprechen.
|
||||
root.helpLastStepButton=Je nach Stand der Algorithmusausführung ändert sich die Funtion des Knopfs. \
|
||||
root.helpLastStepButton=Je nach Stand der Algorithmusausführung ändert sich die FunKtion des Knopfs. \
|
||||
Wenn aktuell der Baum aufgebaut wird, springt die Anzeige nach Klicken des Knopfs vor zum letzten Schritt des \
|
||||
Typherleitungsbaums. Wenn bereits die Unifikation druchgeführt wird, sprigt die Anzeige nach Klicken des Knopfs \
|
||||
vor zur Anzeige des finalen Typs. Der Knopf lässt sich außerdem durch die Tastenkombination \
|
||||
"STRG + Rechte Pfeiltaste" ansprechen.
|
||||
root.helpShareButton=Durch Klicken des Teilen Knopfs öffnet sich ein Dialog, in dem der LaTeX-Code des finalen \
|
||||
Typherleitungsbaums des eingegebenen Terms und die benötigen Pakete zum Einbinden des Latex-Codes angezeigt werden. \
|
||||
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.
|
||||
|
||||
|
@ -46,7 +46,7 @@ By clicking the info-symbol the grammar defining a valid type of a type assmupti
|
||||
is contained in multiple type assumptions, only the uppermost type assumption containing the variable is used for \
|
||||
the algorithm.
|
||||
root.helpFirstStepButton=The function of the button depends on the current state of the algorithm execution. \
|
||||
If the tree is currently built up, clicking on the button shows the first step of the inference tree. \
|
||||
If the tree is currently being built up, clicking on the button shows the first step of the inference tree. \
|
||||
If the unification algorithm is already in progress, clicking on the button shows the last step of the inference \
|
||||
tree. The key combination "CTRL + left arrow key" also executes a click on the button.
|
||||
root.helpPreviousStepButton=By clicking the previous-step button the previous step of the algorithm is shown. \
|
||||
@ -54,7 +54,7 @@ The key combination "left arrow key" also executes a click on the button.
|
||||
root.helpNextStepButton=By clicking the next-step button the next step of the algorithm is shown. \
|
||||
The key combination "right arrow key" also executes a click on the button.
|
||||
root.helpLastStepButton=The function of the button depends on the current state of the algorithm execution. \
|
||||
If the tree is currently built up, clicking on the button shows the last step of the inference tree. \
|
||||
If the tree is currently being built up, clicking on the button shows the last step of the inference tree. \
|
||||
If the unification algorithm is already in progress, clicking on the button shows the final type of the \
|
||||
entered term. The key combination "CTRL + right arrow key" also executes a click on the button.
|
||||
root.helpShareButton=Clicking the share button opens up a dialog containing the LaTeX-code of the final inference \
|
||||
|
@ -15,8 +15,8 @@ class LatexCreatorConstraintsTest {
|
||||
private static final String EMPTY_CONSTRAINT_SET =
|
||||
ALIGN_BEGIN + AMPERSAND + CONSTRAINT_SET + EQUALS + LATEX_CURLY_LEFT + LATEX_CURLY_RIGHT + ALIGN_END;
|
||||
|
||||
private static final String MGU_START = LATEX_NEW_LINE + AMPERSAND + SPLIT_BEGIN + SIGMA + COLON + EQUALS + MGU + PAREN_LEFT
|
||||
+ CONSTRAINT_SET + PAREN_RIGHT;
|
||||
private static final String MGU_START = LATEX_NEW_LINE + AMPERSAND + SPLIT_BEGIN + SIGMA + COLON + EQUALS + MGU
|
||||
+ PAREN_LEFT + CONSTRAINT_SET + PAREN_RIGHT;
|
||||
|
||||
private final Model model = new ModelImpl();
|
||||
private TypeInfererInterface typeInferer;
|
||||
|
Loading…
Reference in New Issue
Block a user