# How to draw "flag format" lambda derivation diagrams as used in the book Type Theory and Formal Proof: An Introduction

I'd like to draw "flag format" diagrams for lambda derivation as used in the book "Type Theory and Formal Proof: An Introduction". Below is an example in Chapter 2 of the book. How can I do it? Thanks. • Welcome! Look at the LaTeX for Logicians website. logicmatters.net/latex-for-logicians/nd : see final comment, 'The flagderiv package can be used to set the variant kind of “flag” proofs some computer scientists like.' If you need further help, please add a minimal working example (MWE).
– cfr
Oct 20, 2019 at 1:27
• Thanks! This is exactly what I want. Oct 20, 2019 at 20:07
• The website I linked is really good for this stuff. If it isn't there, the chances are it isn't available or it isn't logical ;).
– cfr
Oct 20, 2019 at 20:37

As for all things logical, check the LaTeX for Logicians site, find the thing you need and look up the documentation.

Since you've not given any code, I copied an example from page 3 of flagderiv's documentation.

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,flagderiv}

\begin{document}

\begin{flagderiv}
\introduce{in-x}{x: \mathbb{N}}{Introduction of $x$}
\assume{as-x}{x > 5}{Assumption}
\step{big-x}{x > 1}{Arithmetic on \ref{in-x} and \ref{as-x}}
\conclude{conc}{x > 5 \implies x > 1}{$\implies$-intro on \ref{as-x} and \ref{big-x}}
\conclude{}{\forall x \in \mathbb{N}: x > 5 \implies x > 1}{$\forall$-intro on \ref{in-x} and \ref{conc}}
\end{flagderiv}

\end{document} 