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 examples latex code compatible with normal LaTeX

Browse Source
This commit is contained in:
ucrhh 2021-03-05 12:51:56 +01:00
parent b728ced2af
commit a7e8a24d77
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -33,7 +33,7 @@ root.appLatex=\
\ \
\\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\ \\AxiomC{$\\Gamma \\vdash t_2 : \\tau_1$}\
\ \
\\LeftLabel{\\rm A{\\small PP}}\ \\LeftLabel{\\textrm A{\\small PP}}\
\\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\ \\BinaryInfC{$\\Gamma \\vdash t_1 \\ t_2 : \\tau_2$}\
\\end{prooftree} \\end{prooftree}
@ -41,7 +41,7 @@ root.absLatex=\
\\begin{prooftree}\ \\begin{prooftree}\
\\AxiomC{$\\Gamma , \\texttt{x}: \\tau_1 \\vdash t : \\tau_2$}\ \\AxiomC{$\\Gamma , \\texttt{x}: \\tau_1 \\vdash t : \\tau_2$}\
\ \
\\LeftLabel{\\rm A{\\small BS}}\ \\LeftLabel{\\textrm A{\\small BS}}\
\\UnaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\ \\UnaryInfC{$\\Gamma \\vdash \\lambda \\texttt{x}.t : \\tau_1 \\rightarrow \\tau_2$}\
\\end{prooftree} \\end{prooftree}
@ -49,7 +49,7 @@ root.varLatex=\
\\begin{prooftree}\ \\begin{prooftree}\
\\AxiomC{$\\Gamma (\\texttt{x}) = \\tau$}\ \\AxiomC{$\\Gamma (\\texttt{x}) = \\tau$}\
\ \
\\LeftLabel{\\rm V{\\small AR}}\ \\LeftLabel{\\textrm V{\\small AR}}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau'$}\ \\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau'$}\
\\end{prooftree} \\end{prooftree}
@ -57,7 +57,7 @@ root.constLatex=\
\\begin{prooftree}\ \\begin{prooftree}\
\\AxiomC{$\\texttt{c} \\in Const$}\ \\AxiomC{$\\texttt{c} \\in Const$}\
\ \
\\LeftLabel{\\rm C{\\small ONST}}\ \\LeftLabel{\\textrm C{\\small ONST}}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau_c$}\ \\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau_c$}\
\\end{prooftree} \\end{prooftree}
@ -67,7 +67,7 @@ root.letLatex=\
\ \
\\AxiomC{$\\Gamma , \\texttt{x} : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\ \\AxiomC{$\\Gamma , \\texttt{x} : ta(\\tau_1 , \\Gamma ) \\vdash t_2 : \\tau_2$}\
\ \
\\LeftLabel{\\rm L{\\small ET}}\ \\LeftLabel{\\textrm L{\\small ET}}\
\\BinaryInfC{$\\Gamma \\vdash \\textbf{let} \\ \\texttt{x} = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\ \\BinaryInfC{$\\Gamma \\vdash \\textbf{let} \\ \\texttt{x} = t_1 \\ \\textbf{in} \\ t_2 : \\tau_2$}\
\\end{prooftree} \\end{prooftree}
@ -77,6 +77,6 @@ root.varLetLatex=\
\ \
\\AxiomC{$\\tau' \\succeq \\tau$}\ \\AxiomC{$\\tau' \\succeq \\tau$}\
\ \
\\LeftLabel{\\rm V{\\small AR}}\ \\LeftLabel{\\textrm V{\\small AR}}\
\\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\ \\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
\\end{prooftree} \\end{prooftree}