arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 18:30:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

make inference rule appearance consistent with tree appearance

Browse Source
This commit is contained in:
Johanna Stuber 2021-02-05 10:28:06 +01:00
parent 7494407480
commit 2df0107243
3 changed files with 27 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/main/resources/language/general.properties
View File

@ -9,42 +9,50 @@ root.appLatex=\
\
\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\
\
\\LeftLabel{APP}\
\\LeftLabel{\\rm A{\\small PP}}\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
\\end{prooftree}
root.absLatex=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma , x: \\tau_1 \\vdash t : \\tau_2$}\
\\AxiomC{$\\Gamma , \\texttt{x}: \\tau_1 \\vdash t : \\tau_2$}\
\
\\LeftLabel{ABS}\
\\UnaryInfC{$\\Gamma \\vdash \\lambda x.t : \\tau_1 \\rightarrow \\tau_2$}\
\\LeftLabel{\\rm A{\\small BS}}\
\\UnaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
\\end{prooftree}
root.varLatex=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma (x) = \\tau$}\
\\AxiomC{$\\Gamma (\\texttt{x}) = \\tau$}\
\
\\LeftLabel{VAR}\
\\UnaryInfC{$\\Gamma \\vdash x : \\tau'$}\
\\LeftLabel{\\rm V{\\small AR}}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau'$}\
\\end{prooftree}
root.constLatex=\
\\begin{prooftree}\
\\AxiomC{$\\texttt{c} \\in Const$}\
\
\\LeftLabel{\\rm C{\\small ONST}}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau_c$}\
\\end{prooftree}
root.letLatex=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma \\vdash t_1 : \\tau_1$}\
\
\\AxiomC{$\\Gamma , x : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\
\\AxiomC{$\\Gamma , \\texttt{x} : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\
\
\\LeftLabel{APP}\
\\BinaryInfC{$\\Gamma \\vdash\ \\textbf{let} \\ x = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\
\\LeftLabel{\\rm L{\\small ET}}\
\\BinaryInfC{$\\Gamma \\vdash\ \\textbf{let} \\ \\texttt{x} = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\
\\end{prooftree}
root.varLetLatex=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma (x) = \\tau'$}\
\\AxiomC{$\\Gamma (\\texttt{x}) = \\tau'$}\
\
\\AxiomC{$\\tau' \\succeq \\tau$}\
\
\\LeftLabel{VAR}\
\\BinaryInfC{$\\Gamma \\vdash x : \\tau$}\
\\LeftLabel{\\rm V{\\small AR}}\
\\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
\\end{prooftree}

14
src/main/resources/language/translation_de.properties
View File

@ -17,22 +17,14 @@ root.german=Deutsch
root.english=Englisch
root.selectLanguage=Sprache
root.constLatex=\
\\begin{prooftree}\
\\AxiomC{\\texttt{c ist eine Konstante}}\
\
\\LeftLabel{CONST}\
\\UnaryInfC{$\\Gamma \\vdash c : \\tau_c$}\
\\end{prooftree}
root.absLetLatex=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma , x: \\tau_1 \\vdash t : \\tau_2$}\
\\AxiomC{$\\Gamma , \\texttt{x}: \\tau_1 \\vdash t : \\tau_2$}\
\
\\AxiomC{$\\tau_1$ \\ \\texttt{kein Typschema}}\
\
\\LeftLabel{ABS}\
\\BinaryInfC{$\\Gamma \\vdash \\lambda x.t : \\tau_1 \\rightarrow \\tau_2$}\
\\LeftLabel{\\rm A{\\small BS}}\
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
\\end{prooftree}
demo-tree=\

14
src/main/resources/language/translation_en.properties
View File

@ -17,22 +17,14 @@ root.german=German
root.english=English
root.selectLanguage=Language
root.constLatex=\
\\begin{prooftree}\
\\AxiomC{\\texttt{c is a constant}}\
\
\\LeftLabel{CONST}\
\\UnaryInfC{$\\Gamma \\vdash c : \\tau_c$}\
\\end{prooftree}
root.absLetLatex=\
\\begin{prooftree}\
\\AxiomC{$\\Gamma , x: \\tau_1 \\vdash t : \\tau_2$}\
\\AxiomC{$\\Gamma , \\texttt{x}: \\tau_1 \\vdash t : \\tau_2$}\
\
\\AxiomC{$\\tau_1$ \\ \\texttt{no type scheme}}\
\
\\LeftLabel{ABS}\
\\BinaryInfC{$\\Gamma \\vdash \\lambda x.t : \\tau_1 \\rightarrow \\tau_2$}\
\\LeftLabel{\\rm A{\\small BS}}\
\\BinaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
\\end{prooftree}
demo-tree=\