mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
addition to ass grammar, unification error strings
This commit is contained in:
parent
d6bc8bb9cd
commit
56185806d7
@ -284,8 +284,9 @@ public class LatexCreatorConstraints implements StepVisitor {
|
|||||||
latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length());
|
latex.delete(latex.length() - LATEX_NEW_LINE.length(), latex.length());
|
||||||
latex.append(SPLIT_END);
|
latex.append(SPLIT_END);
|
||||||
if (error.isPresent()) {
|
if (error.isPresent()) {
|
||||||
latex.append(LATEX_NEW_LINE + AMPERSAND);
|
latex.append(LATEX_NEW_LINE + LATEX_NEW_LINE + AMPERSAND + TEXT + CURLY_LEFT);
|
||||||
latex.append(translationProvider.apply(error.get()));
|
latex.append(translationProvider.apply(error.get()));
|
||||||
|
latex.append(CURLY_RIGHT);
|
||||||
}
|
}
|
||||||
steps.add(latex.toString());
|
steps.add(latex.toString());
|
||||||
}
|
}
|
||||||
|
@ -23,7 +23,7 @@ root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2
|
|||||||
|
|
||||||
root.assGrammar=\u2329Type\u232A ::= (\u2329Type\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \
|
root.assGrammar=\u2329Type\u232A ::= (\u2329Type\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \
|
||||||
\u2329FunctionType\u232A <br> \
|
\u2329FunctionType\u232A <br> \
|
||||||
\u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]* <br> \
|
\u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]*  \\t[0-9]+ <br> \
|
||||||
\u2329VarType\u232A ::= t[0-9]+ <br> \
|
\u2329VarType\u232A ::= t[0-9]+ <br> \
|
||||||
\u2329FunctionType\u232A ::= \u2329Type\u232A -> \u2329Type\u232A
|
\u2329FunctionType\u232A ::= \u2329Type\u232A -> \u2329Type\u232A
|
||||||
|
|
||||||
|
@ -112,6 +112,11 @@ root.absLetLatex=\
|
|||||||
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
|
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
|
||||||
\\end{prooftree}
|
\\end{prooftree}
|
||||||
|
|
||||||
|
root.infinite_type = Der eingegebene Term ist nicht typisierbar: \
|
||||||
|
Durch den hervorgehobenen Constraint würde sich ein unendlicher Typ ergeben!
|
||||||
|
root.different_types = Der eingegebene Term ist nicht typisierbar: \
|
||||||
|
In dem hervorgehobenen Constraint werden zwei unvereinbare Typen gleichgesetzt!
|
||||||
|
|
||||||
share.url.label=URL
|
share.url.label=URL
|
||||||
share.packages.label=Pakete
|
share.packages.label=Pakete
|
||||||
share.latex.label=LaTeX-Code
|
share.latex.label=LaTeX-Code
|
||||||
|
@ -105,6 +105,11 @@ root.absLetLatex=\
|
|||||||
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
|
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
|
||||||
\\end{prooftree}
|
\\end{prooftree}
|
||||||
|
|
||||||
|
root.infinite_type = The entered term cannot be typed: \
|
||||||
|
The highlighted Constraint would cause an infinite type!
|
||||||
|
root.different_types = The entered term cannot be typed: \
|
||||||
|
The highlighted Constraint contains two incompatible types!
|
||||||
|
|
||||||
share.url.label=URL
|
share.url.label=URL
|
||||||
share.packages.label=Packages
|
share.packages.label=Packages
|
||||||
share.latex.label=LaTeX code
|
share.latex.label=LaTeX code
|
||||||
|
Loading…
Reference in New Issue
Block a user