Add rulenameAfter command

This commit is contained in:
Andreas Stadelmeier 2024-04-24 17:30:15 +02:00
parent 585254d814
commit 76b800d953
2 changed files with 12 additions and 4 deletions

View File

@ -41,12 +41,18 @@ this.<List<String>>emptyList().add(new List<String>())
\end{verbatim} \end{verbatim}
$ $
\begin{array}{c} \begin{array}[b]{c}
TODO \begin{array}[b]{c}
\texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}}
\\ \\
\hline \hline
\texttt{emptyList().get().get()} : \tv{a} \texttt{emptyList().get()} : \exptype{List}{\type{String}}
\end{array} \quad \rulename{T-Call} \end{array} \rulenameAfter{T-Call}
\quad \generics{\type{X}}\exptype{List}{\type{X}} \to \type{X} \in \mtypeEnvironment{}(\texttt{get})1
\\
\hline
\texttt{emptyList().get().get()} : \type{String}
\end{array} \rulenameAfter{T-Call}
$ $
%motivate constraints: %motivate constraints:

View File

@ -19,6 +19,8 @@
\newtheorem{recap}[note]{Recap} \newtheorem{recap}[note]{Recap}
\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
\newcommand{\tifj}{\texttt{TamedFJ}} \newcommand{\tifj}{\texttt{TamedFJ}}
\newcommand{\wcSep}{\vdash} \newcommand{\wcSep}{\vdash}