\(\lambda\)

Autor

Enric Cosme Llópez

Publicat

March 5, 2021

TT.tex
\documentclass[border=1cm]{standalone}
\usepackage{pgfplots} 
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usetikzlibrary{shapes.geometric, arrows,arrows.meta}
\usetikzlibrary{decorations.markings}
 
\begin{document}
\centering
\begin{tikzpicture}
[Lin/.style={-, line width=1pt}, scale=0.8]
\draw[Lin] (0,0) to node [] {} (3,0);
\node[] () at (1.6,.3) [] {$\Gamma \vdash y\colon \alpha \to \beta$};
\node[] () at (3.6,0) [] {(var)};

\draw[Lin] (5,0) to node [] {} (8,0);
\node[] () at (6.7,.35) [] {$\Gamma \vdash z\colon \alpha $};
\node[] () at (8.6,0) [] {(var)};

\draw[Lin] (1,-1) to node [] {} (7,-1);
\node[] () at (4.3,-.65) [] {$\Gamma \vdash yz\colon \beta$};
\node[] () at (7.7,-1) [] {(appl)};

\draw[Lin] (-.5,-2) to node [] {} (8.5,-2);
\node[] () at (4.3,-1.65) [] {$y\colon \alpha\to \beta \vdash \lambda z, yz\colon \alpha \to \beta$};
\node[] () at (9.2,-2) [] {(abst)};

\node[] () at (4.3,-2.65) [] {$\emptyset\vdash \lambda y\colon \alpha\to\beta, \lambda z\colon\alpha, yz\colon (\alpha\to\beta)\to \alpha\to\beta$};
\end{tikzpicture}
\end{document}