|
| 1 | +# Curryst |
| 2 | + |
| 3 | +A Typst package for typesetting proof trees. |
| 4 | + |
| 5 | + |
| 6 | +## Import |
| 7 | + |
| 8 | +You can import the latest version of this package with: |
| 9 | + |
| 10 | +```typst |
| 11 | +#import "@preview/curryst:0.4.0": rule, proof-tree |
| 12 | +``` |
| 13 | + |
| 14 | +## Basic usage |
| 15 | + |
| 16 | +To display a proof tree, you first need to create a tree, using the `rule` function. Its first argument is the conclusion, and the other positional arguments are the premises. It also accepts a `name` for the rule name, displayed on the right of the bar, as well as a `label`, displayed on the left of the bar. |
| 17 | + |
| 18 | +```typ |
| 19 | +#let tree = rule( |
| 20 | + label: [Label], |
| 21 | + name: [Rule name], |
| 22 | + [Conclusion], |
| 23 | + [Premise 1], |
| 24 | + [Premise 2], |
| 25 | + [Premise 3] |
| 26 | +) |
| 27 | +``` |
| 28 | + |
| 29 | +Then, you can display the tree with the `proof-tree` function: |
| 30 | + |
| 31 | +```typ |
| 32 | +#proof-tree(tree) |
| 33 | +``` |
| 34 | + |
| 35 | +In this case, we get the following result: |
| 36 | + |
| 37 | + |
| 38 | + |
| 39 | +Proof trees can be part of mathematical formulas: |
| 40 | + |
| 41 | +```typ |
| 42 | +Consider the following tree: |
| 43 | +$ |
| 44 | + Pi quad = quad #proof-tree( |
| 45 | + rule( |
| 46 | + $phi$, |
| 47 | + $Pi_1$, |
| 48 | + $Pi_2$, |
| 49 | + ) |
| 50 | + ) |
| 51 | +$ |
| 52 | +$Pi$ constitutes a derivation of $phi$. |
| 53 | +``` |
| 54 | + |
| 55 | + |
| 56 | + |
| 57 | +You can specify a rule as the premises of a rule in order to create a tree: |
| 58 | + |
| 59 | +```typ |
| 60 | +#proof-tree( |
| 61 | + rule( |
| 62 | + name: $R$, |
| 63 | + $C_1 or C_2 or C_3$, |
| 64 | + rule( |
| 65 | + name: $A$, |
| 66 | + $C_1 or C_2 or L$, |
| 67 | + rule( |
| 68 | + $C_1 or L$, |
| 69 | + $Pi_1$, |
| 70 | + ), |
| 71 | + ), |
| 72 | + rule( |
| 73 | + $C_2 or overline(L)$, |
| 74 | + $Pi_2$, |
| 75 | + ), |
| 76 | + ) |
| 77 | +) |
| 78 | +``` |
| 79 | + |
| 80 | + |
| 81 | + |
| 82 | +As an example, here is a natural deduction proof tree generated with Curryst: |
| 83 | + |
| 84 | + |
| 85 | + |
| 86 | +<details> |
| 87 | + <summary>Show code</summary> |
| 88 | + |
| 89 | + ```typ |
| 90 | + #let ax = rule.with(name: [ax]) |
| 91 | + #let and-el = rule.with(name: $and_e^ell$) |
| 92 | + #let and-er = rule.with(name: $and_e^r$) |
| 93 | + #let impl-i = rule.with(name: $scripts(->)_i$) |
| 94 | + #let impl-e = rule.with(name: $scripts(->)_e$) |
| 95 | + #let not-i = rule.with(name: $not_i$) |
| 96 | + #let not-e = rule.with(name: $not_e$) |
| 97 | +
|
| 98 | + #proof-tree( |
| 99 | + impl-i( |
| 100 | + $tack (p -> q) -> not (p and not q)$, |
| 101 | + not-i( |
| 102 | + $p -> q tack not (p and not q)$, |
| 103 | + not-e( |
| 104 | + $ underbrace(p -> q\, p and not q, Gamma) tack bot $, |
| 105 | + impl-e( |
| 106 | + $Gamma tack q$, |
| 107 | + ax($Gamma tack p -> q$), |
| 108 | + and-el( |
| 109 | + $Gamma tack p$, |
| 110 | + ax($Gamma tack p and not q$), |
| 111 | + ), |
| 112 | + ), |
| 113 | + and-er( |
| 114 | + $Gamma tack not q$, |
| 115 | + ax($Gamma tack p and not q$), |
| 116 | + ), |
| 117 | + ), |
| 118 | + ), |
| 119 | + ) |
| 120 | + ) |
| 121 | + ``` |
| 122 | +</details> |
| 123 | + |
| 124 | + |
| 125 | +## Advanced usage |
| 126 | + |
| 127 | +The `proof-tree` function accepts multiple named arguments that let you customize the tree: |
| 128 | + |
| 129 | +<dl> |
| 130 | + <dt><code>prem-min-spacing</code></dt> |
| 131 | + <dd>The minimum amount of space between two premises.</dd> |
| 132 | + |
| 133 | + <dt><code>title-inset</code></dt> |
| 134 | + <dd>The amount width with which to extend the horizontal bar beyond the content. Also determines how far from the bar labels and names are displayed.</dd> |
| 135 | + |
| 136 | + <dt><code>stroke</code></dt> |
| 137 | + <dd>The stroke to use for the horizontal bars.</dd> |
| 138 | + |
| 139 | + <dt><code>horizontal-spacing</code></dt> |
| 140 | + <dd>The space between the bottom of the bar and the conclusion, and between the top of the bar and the premises.</dd> |
| 141 | + |
| 142 | + <dt><code>min-bar-height</code></dt> |
| 143 | + <dd>The minimum height of the box containing the horizontal bar.</dd> |
| 144 | + |
| 145 | + <dt><code>dir</code></dt> |
| 146 | + <dd>The orientation of the proof tree (either <code>btt</code> or <code>ttb</code>, <code>btt</code> being the default).</dd> |
| 147 | +</dl> |
| 148 | + |
| 149 | +For more information, please refer to the documentation in [`curryst.typ`](curryst.typ). |
0 commit comments