This package is for constructing proof trees in the style of natural deduction or the sequent calculus, for typst
0.7.0
. Please do open issues for bugs etc :)
Features:
¹ The placement of labels is currently very primitive, and requires much user intervention.
² Options are quite limited.
The user interface is inspired by bussproof's; a tree is constructed by a sequence of 'lines' that state their number of premises.
src/prooftrees.typ
contains the documentation and the main functions needed.
The code for some example trees can be seen in examples/prooftree_test.typ
.
A single inference would be:
#import "@preview/prooftrees:0.1.0"
#prooftree.tree(
prooftree.axi[$A => A$],
prooftree.uni[$A => A, B$]
)
A more interesting example:
#import "@preview/prooftrees:0.1.0"
#prooftree.tree(
prooftree.axi[$B => B$],
prooftree.uni[$B => B, A$],
prooftree.uni[$B => A, B$],
prooftree.axi[$A => A$],
prooftree.uni[$A => A, B$],
prooftree.bin[$B => A, B$]
)
An n-ary inference can be made:
#import "@preview/prooftrees:0.1.0"
#prooftrees.tree(
prooftrees.axi(pad(bottom: 2pt, [$P_1$])),
prooftrees.axi(pad(bottom: 2pt, [$P_2$])),
prooftrees.axi(pad(bottom: 2pt, [$P_3$])),
prooftrees.axi(pad(bottom: 2pt, [$P_4$])),
prooftrees.axi(pad(bottom: 2pt, [$P_5$])),
prooftrees.axi(pad(bottom: 2pt, [$P_6$])),
prooftrees.nary(6)[$C$],
)
The boundaries of blocks containing math do not expand enough for sub/pscripts; I think this is a typst issue. Short-term fix: add manual vspace or padding in the cell.
The placement of the line and conclusion is calculated using measure
on the premises and labels, and doing geometric arithmetic with these values.