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

by markeric   Last Updated October 20, 2019 02:23 AM

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.

Flag format

Answers 1

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.



  \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}}


flagged derivation

October 20, 2019 01:43 AM

Related Questions

Updated August 05, 2015 13:10 PM

Updated June 08, 2016 08:09 AM

Updated June 10, 2017 04:23 AM

Updated September 22, 2017 21:23 PM

Updated September 17, 2017 20:23 PM