typst-prooftree

typst-prooftree allows you to draw proof trees in Typst. Heavily inspired by Latex's bussproofs package.

Feel free to open an issue or a pull request if you have a question or there's something missing you would like to see.

Getting started

Copy the prooftree.typ file to your project or add this repository as a submodule to yours. Then you just need:

#import "path/to/prooftree.typ": *

at the top of your current file and you're ready to go!

Example

You can generate the image above with the following code:

#import "path/to/prooftree.typ": *

#prooftree(
  axiom("A"),
  rule("B"),
  axiom("C"),
  rule(n: 2, "D"),
  axiom("E"),
  axiom("F"),
  rule(n: 2, "G"),
  rule("H"),
  rule(n: 2, "I")
)

How it works

prooftree

let prooftree(
  spacing: (
    horizontal: 1em,
    vertical: 0.5em,
    lateral: 0.5em,
  ),
  label: (
    side: left,
    padding: 0.2em,
  ),
  line-stroke: 0.5pt,
  ..rules
) = /* ... */

The main function exported by this library is prooftree. If you're familiar with bussproofs, this function acts like its prooftree environment. prooftree describes the proof tree like a stack, taking its elements as positional arguments. axioms gets pushed into a stack and become the leaves, while rules pop trees from such stack, combine them into a new tree and push them back, becoming the middle nodes.

Moreover this functions takes the following named arguments:

• spacing: a dictionary of spacing related arguments, in particular:
  • horizontal or h: lengths that regulate the horizontal spacing between sibling rules (default: 1em).
  • vertical or v: lengths that regulate the vertical spacing between the rules and the horizontal lines (default: 0.5em);
  • lateral or l: lengths that regulate the horizontal spacing on the sides of each rules (default: 0.5em); the difference between this and horizontal is that this spacing enlarges the horizontal lines.
• label: a dictionary of label related arguments, in particular:
  • side: alignment that regulates the default side of labels on rules, but not axioms (default: left). Possible values are left and right;
  • padding: length that regulates the distance between the label and the rule (default: 0.2em).
• line-stroke: length that regulates the thickness of lines on rules (default: 0.5pt).

axiom

let axiom(label: none, body) = /* ... */

axiom's job is to describe the leaves of the proof tree. It takes the following arguments:

• label: a named argument containing the label of the axiom. This can be none (default) or a string or content, containing the actual label to display;
• body: a positional argument containing the body of the axiom. Can be anything and will be displayed as is.

rule

let rule(n: 1, label: none, root) = /* ... */

rule pops a given number of proof trees from the prooftree's stack and adds a common root to them. It takes the following arguments:

• n: a named argument representing the number of proof trees to pop (default: 1). Currently n: 0 is equivalent to using axiom, but this may change in the future;
• label: a named argument representing the label(s) to show. It can be either:
  • none, in which case no label is shown;
  • a string or content, in which case a label is shown on the default side of the prooftree;
  • a dictionary having left and/or right as keys, in which case the values associated to each key will be shown on the relative side.