Tcolorbox and logic formats

Question

I asked chatGPT4 to reproduce something like this with the tcolorbox and bussproofs packages:

However, the code it gave me doesn't quite do the trick. I've been trying to change it but no success so far. Here's the code and what it looks like:

\begin{tcolorbox}[colback=gray!10!white, colframe=gray!70!black, title=STLC]

\begin{minipage}{0.5\textwidth}
    \textbf{Syntax}
        \[
            \begin{array}{r l}
            t ::=\\
                 & x \quad \text{variable} \\
                 & \lambda x.t \quad \text{abstraction} \\
                 & t \, t \quad \text{application} \\
            \end{array}
        \]
\end{minipage}

\vspace{0.5cm}

\begin{minipage}{0.5\textwidth}
    \textbf{Values}
    \[
        \begin{array}{r l}
            v ::= & \lambda x.t \quad \text{abstraction value} \\
        \end{array}
    \]
\end{minipage}

\vspace{0.5cm}

\textbf{Evaluation}
\[
\begin{array}{c}
    \infer[\text{E-App1}]{t_1 t_2 \to t_1' t_2}{t_1 \to t_1'}
    \\[10pt]
    \infer[\text{E-App2}]{v_1 t_2 \to v_1 t_2'}{t_2 \to t_2'}
    \\[10pt]
    \infer[\text{E-AppAbs}]{(\lambda x.t_{12}) v_2 \to [x \mapsto v_2]t_{12}}{}
\end{array}
\]

\end{tcolorbox}

Can I get some help with this?

Thanks!

Answer 1

You should provide complete MWE, from your code fragment is not clear which package you use and how you imagine that inrefer should be formulated (standard proof package not support showed result).

So below is code which reproduce shoved desired image, but I'm not sure if this result is correct ...

\documentclass{article}
\usepackage[many]{tcolorbox}
\usepackage{proof}
\usepackage{tabularray}
\UseTblrLibrary{booktabs}
                
\begin{document}
\begin{tcolorbox}[colback=gray!10!white, colframe=gray!70!black, 
                  title=STLC]
\textbf{Syntax}

    \begin{tblr}{colspec = {Q[r, mode=math] Q[l, mode=math] X[r]},
                 rowsep=1pt}
t ::=   &               &   terms:              \\
        & x             &   variable            \\
        & \lambda x.t   &   abstraction         \\
        & t\, t         &   application         \\
    \addlinespace
v ::=   &               &   values              \\     
        & \lambda x.t   &   abstraction value   \\
    \end{tblr}
\bigskip
\textbf{Evaluation}

    \begin{tblr}{colsep=1pt,
                 colspec = {r Q[l, mode=dmath]},
                 rowsep=7pt}
E-App1      &   \dfrac{t_1 t_2 \to t_1' t_2}{t_1 \to t_1'}      \\
E-App2      &   \dfrac{v_1 t_2 \to v_1 t_2'}{t_2 \to t_2'}      \\
E-AppAbs    &   \dfrac{~}{(\lambda x,t_{12})v_2 \to [x \mapsto v_2]t_{12}}
    \end{tblr}
\end{tcolorbox}
\end{document}