Skip to content

Commit ab901cf

Browse files
pauladam94pauladam94
authored
curryst:0.6.0 (#3452)
1 parent 4192704 commit ab901cf

File tree

9 files changed

+2813
-0
lines changed

9 files changed

+2813
-0
lines changed

‎packages/preview/curryst/0.6.0/LICENSE‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MIT License
2+
3+
Copyright (c) 2025 Rémi Hutin - Paul Adam - Malo <@MDLC01>
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
The above copyright notice and this permission notice shall be included in all
13+
copies or substantial portions of the Software.
14+
15+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+
SOFTWARE.

‎packages/preview/curryst/0.6.0/README.md‎

Lines changed: 218 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,218 @@
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.6.0": rule, prooftree, rule-set
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+
[Premise 1],
23+
[Premise 2],
24+
[Premise 3],
25+
[Conclusion],
26+
)
27+
```
28+
29+
Then, you can display the tree with the `prooftree` function:
30+
31+
```typ
32+
#prooftree(tree)
33+
```
34+
35+
In this case, we get the following result:
36+
37+
![A proof tree with three premises, a conclusion, and a rule name.](examples/usage.svg)
38+
39+
Proof trees can be part of mathematical formulas:
40+
41+
```typ
42+
Consider the following tree:
43+
$
44+
Pi quad = quad prooftree(
45+
rule(
46+
Pi_1,
47+
Pi_2,
48+
phi,
49+
)
50+
)
51+
$
52+
$Pi$ constitutes a derivation of $phi$.
53+
```
54+
55+
![The rendered document.](examples/math-formula.svg)
56+
57+
You can specify a rule as the premises of a rule in order to create a tree:
58+
59+
```typ
60+
#prooftree(
61+
rule(
62+
name: $R$,
63+
rule(
64+
name: $A$,
65+
rule(
66+
$Pi_1$,
67+
$C_1 or L$,
68+
),
69+
$C_1 or C_2 or L$,
70+
),
71+
rule(
72+
$Pi_2$,
73+
$C_2 or overline(L)$,
74+
),
75+
$C_1 or C_2 or C_3$,
76+
)
77+
)
78+
```
79+
80+
![The rendered tree.](examples/rule-as-premise.svg)
81+
82+
As an example, here is a natural deduction proof tree generated with Curryst:
83+
84+
![The rendered tree.](examples/natural-deduction.svg)
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+
#prooftree(
99+
impl-i(
100+
not-i(
101+
not-e(
102+
impl-e(
103+
ax($Gamma tack p -> q$),
104+
and-el(
105+
ax($Gamma tack p and not q$),
106+
$Gamma tack p$,
107+
),
108+
$Gamma tack q$,
109+
),
110+
and-er(
111+
ax($Gamma tack p and not q$),
112+
$Gamma tack not q$,
113+
),
114+
$ underbrace(p -> q\, p and not q, Gamma) tack bot $,
115+
),
116+
$p -> q tack not (p and not q)$,
117+
),
118+
$tack (p -> q) -> not (p and not q)$,
119+
)
120+
)
121+
```
122+
</details>
123+
124+
125+
## Advanced usage
126+
127+
The `prooftree` function accepts multiple named arguments that let you customize the tree:
128+
129+
<dl>
130+
<dt><code>min-premise-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 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>vertical-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).
150+
151+
## Layout Multiple Rules (a simple way)
152+
153+
Here we show a way to typeset multiple rules at one time :
154+
155+
![8 rules rendered together.](examples/rule-set.svg)
156+
<details>
157+
<summary>Show code</summary>
158+
159+
```typ
160+
#let variable = prooftree(rule(
161+
name: [Variable],
162+
$Gamma, x : A tack x : A$,
163+
))
164+
#let abstraction = prooftree(rule(
165+
name: [Abstraction],
166+
$Gamma, x: A tack P : B$,
167+
$Gamma tack lambda x . P : A => B$,
168+
))
169+
170+
#let application = prooftree(rule(
171+
name: [Application],
172+
$Gamma tack P : A => B$,
173+
$Delta tack Q : B$,
174+
$Gamma, Delta tack P Q : B$,
175+
))
176+
177+
#let weakening = prooftree(rule(
178+
name: [Weakening],
179+
$Gamma tack P : B$,
180+
$Gamma, x : A tack P : B$,
181+
))
182+
183+
#let contraction = prooftree(rule(
184+
label: [Contraction],
185+
$Gamma, x : A, y : A tack P : B$,
186+
$Gamma, z : A tack P[x, y <- z]: B$,
187+
))
188+
189+
#let exchange = prooftree(rule(
190+
label: [Exchange],
191+
$Gamma, x : A, y: B, Delta tack P : B$,
192+
$Gamma, y : B, x: A, Delta tack P : B$,
193+
))
194+
195+
#align(center, rule-set(
196+
variable,
197+
abstraction,
198+
application,
199+
weakening,
200+
contraction,
201+
exchange
202+
))
203+
```
204+
</details>
205+
206+
207+
The function `rule-set` is very simple and is implemented this way :
208+
209+
```typ
210+
#let rule-set(column-gutter: 3em, row-gutter: 2em, ..rules) = {
211+
set par(leading: row-gutter)
212+
block(rules.pos().map(box).join(h(column-gutter, weak: true)))
213+
}
214+
```
215+
216+
To have more complex layout you can modify this piece of code at your linking.
217+
However the `curryst` package is not meant right now for layout of arbritary content
218+
and other packages do it better for more fine grained customization.

0 commit comments

Comments
 (0)