diff --git a/packages/preview/curryst/0.4.0/LICENSE b/packages/preview/curryst/0.4.0/LICENSE new file mode 100644 index 000000000..6976043b5 --- /dev/null +++ b/packages/preview/curryst/0.4.0/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2025 Rémi Hutin - Paul Adam - Malo <@MDLC01> + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/packages/preview/curryst/0.4.0/README.md b/packages/preview/curryst/0.4.0/README.md new file mode 100644 index 000000000..b6e47d75e --- /dev/null +++ b/packages/preview/curryst/0.4.0/README.md @@ -0,0 +1,149 @@ +# Curryst + +A Typst package for typesetting proof trees. + + +## Import + +You can import the latest version of this package with: + +```typst +#import "@preview/curryst:0.4.0": rule, proof-tree +``` + +## Basic usage + +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. + +```typ +#let tree = rule( + label: [Label], + name: [Rule name], + [Conclusion], + [Premise 1], + [Premise 2], + [Premise 3] +) +``` + +Then, you can display the tree with the `proof-tree` function: + +```typ +#proof-tree(tree) +``` + +In this case, we get the following result: + +![A proof tree with three premises, a conclusion, and a rule name.](examples/usage.svg) + +Proof trees can be part of mathematical formulas: + +```typ +Consider the following tree: +$ + Pi quad = quad #proof-tree( + rule( + $phi$, + $Pi_1$, + $Pi_2$, + ) + ) +$ +$Pi$ constitutes a derivation of $phi$. +``` + +![The rendered document.](examples/math-formula.svg) + +You can specify a rule as the premises of a rule in order to create a tree: + +```typ +#proof-tree( + rule( + name: $R$, + $C_1 or C_2 or C_3$, + rule( + name: $A$, + $C_1 or C_2 or L$, + rule( + $C_1 or L$, + $Pi_1$, + ), + ), + rule( + $C_2 or overline(L)$, + $Pi_2$, + ), + ) +) +``` + +![The rendered tree.](examples/rule-as-premise.svg) + +As an example, here is a natural deduction proof tree generated with Curryst: + +![The rendered tree.](examples/natural-deduction.svg) + +
+ Show code + + ```typ + #let ax = rule.with(name: [ax]) + #let and-el = rule.with(name: $and_e^ell$) + #let and-er = rule.with(name: $and_e^r$) + #let impl-i = rule.with(name: $scripts(->)_i$) + #let impl-e = rule.with(name: $scripts(->)_e$) + #let not-i = rule.with(name: $not_i$) + #let not-e = rule.with(name: $not_e$) + + #proof-tree( + impl-i( + $tack (p -> q) -> not (p and not q)$, + not-i( + $p -> q tack not (p and not q)$, + not-e( + $ underbrace(p -> q\, p and not q, Gamma) tack bot $, + impl-e( + $Gamma tack q$, + ax($Gamma tack p -> q$), + and-el( + $Gamma tack p$, + ax($Gamma tack p and not q$), + ), + ), + and-er( + $Gamma tack not q$, + ax($Gamma tack p and not q$), + ), + ), + ), + ) + ) + ``` +
+ + +## Advanced usage + +The `proof-tree` function accepts multiple named arguments that let you customize the tree: + +
+
prem-min-spacing
+
The minimum amount of space between two premises.
+ +
title-inset
+
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.
+ +
stroke
+
The stroke to use for the horizontal bars.
+ +
horizontal-spacing
+
The space between the bottom of the bar and the conclusion, and between the top of the bar and the premises.
+ +
min-bar-height
+
The minimum height of the box containing the horizontal bar.
+ +
dir
+
The orientation of the proof tree (either btt or ttb, btt being the default).
+
+ +For more information, please refer to the documentation in [`curryst.typ`](curryst.typ). diff --git a/packages/preview/curryst/0.4.0/curryst.typ b/packages/preview/curryst/0.4.0/curryst.typ new file mode 100644 index 000000000..da59ec122 --- /dev/null +++ b/packages/preview/curryst/0.4.0/curryst.typ @@ -0,0 +1,495 @@ +/// Creates an inference rule. +/// +/// You can render a rule created with this function using the `proof-tree` +/// function. +#let rule( + /// The label of the rule, displayed on the left of the horizontal bar. + label: none, + /// The name of the rule, displayed on the right of the horizontal bar. + name: none, + /// The conclusion of the rule. + conclusion, + /// The premises of the rule. Might be other rules constructed with this + /// function, or some content. + ..premises +) = { + assert( + label == none or type(label) in (str, content, symbol), + message: "the label of a rule must be some content", + ) + assert( + name == none or type(name) in (str, content, symbol), + message: "the name of a rule must be some content", + ) + assert( + type(conclusion) in (str, content, symbol), + message: "the conclusion of a rule must be some content (it cannot be another rule)", + ) + for premise in premises.pos() { + assert( + type(premise) in (str, content, symbol) + or ( + type(premise) == dictionary + and "name" in premise + and "conclusion" in premise + and "premises" in premise + ), + message: "a premise must be some content or another rule", + ) + } + assert.eq( + premises.named().len(), + 0, + message: "unexpected named arguments to `rule`", + ) + ( + label: label, + name: name, + conclusion: conclusion, + premises: premises.pos() + ) +} + +/// Lays out a proof tree. +#let proof-tree( + /// The rule to lay out. + /// + /// Such a rule can be constructed using the `rule` function. + rule, + /// The minimum amount of space between two premises. + prem-min-spacing: 15pt, + /// 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. + title-inset: 2pt, + /// The stroke to use for the horizontal bars. + stroke: stroke(0.4pt), + /// The space between the bottom of the bar and the conclusion, and between + /// the top of the bar and the premises. + /// + /// Note that, in this case, "the bar" refers to the bounding box of the + /// horizontal line and the rule name (if any). + horizontal-spacing: 0pt, + /// The minimum height of the box containing the horizontal bar. + /// + /// The height of this box is normally determined by the height of the rule + /// name because it is the biggest element of the box. This setting lets you + /// set a minimum height. The default is 0.8em, is higher than a single line + /// of content, meaning all parts of the tree will align properly by default, + /// even if some rules have no name (unless a rule is higher than a single + /// line). + min-bar-height: 0.8em, + /// The orientation of the proof tree. + /// + /// If set to ttb, the conclusion will be at the top, and the premises will + /// be at the bottom. Defaults to btt, the conclusion being at the bottom + /// and the premises at the top. + dir: btt, +) = { + /// Lays out some content. + /// + /// This function simply wraps the passed content in the usual + /// `(content: .., left-blank: .., right-blank: ..)` dictionary. + let layout-content(content) = { + // We wrap the content in a box with fixed dimensions so that fractional units + // don't come back to haunt us later. + let dimensions = measure(content) + ( + content: box( + // stroke: yellow + 0.3pt, // DEBUG + ..dimensions, + content, + ), + left-blank: 0pt, + right-blank: 0pt, + ) + } + + + /// Lays out multiple premises, spacing them properly. + let layout-premises( + /// Each laid out premise. + /// + /// Must be an array of ditionaries with `content`, `left-blank` and + /// `right-blank` attributes. + premises, + /// The minimum amount between each premise. + min-spacing, + /// If the laid out premises have an inner width smaller than this, their + /// spacing will be increased in order to reach this inner width. + optimal-inner-width, + ) = { + let arity = premises.len() + + if arity == 0 { + return layout-content(none) + } + + if arity == 1 { + return premises.at(0) + } + + let left-blank = premises.at(0).left-blank + let right-blank = premises.at(-1).right-blank + + let initial-content = stack( + dir: ltr, + spacing: min-spacing, + ..premises.map(premise => premise.content), + ) + let initial-inner-width = measure(initial-content).width - left-blank - right-blank + + if initial-inner-width >= optimal-inner-width { + return ( + content: box(initial-content), + left-blank: left-blank, + right-blank: right-blank, + ) + } + + // Conclusion is wider than the premises: they need to be spaced out. + let remaining-space = optimal-inner-width - initial-inner-width + let final-content = stack( + dir: ltr, + spacing: min-spacing + remaining-space / (arity + 1), + ..premises.map(premise => premise.content), + ) + + ( + content: box(final-content), + left-blank: left-blank, + right-blank: right-blank, + ) + } + + + /// Lays out multiple premises that are all leaves, spacing them properly, and + /// optionally creating multiple lines if there is not enough available + /// horizontal space. + let layout-leaf-premises( + /// Each laid out premise. + /// + /// Must be an array of content-like (meaning `content`, `string`, etc.). + premises, + /// The minimum amount between each premise. + min-spacing, + /// If the laid out premises have an inner width smaller than this, their + /// spacing will be increased in order to reach this inner width. + optimal-inner-width, + /// The available width for the returned content. + /// + /// `none` is interpreted as infinite available width. + /// + /// Ideally, the width of the returned content should be bounded by this + /// value, although no guarantee is made. + available-width, + ) = { + // By default, typeset like a regular tree. + + let default = layout-premises( + premises.map(layout-content), + min-spacing, + optimal-inner-width, + ) + + if available-width == none or measure(default.content).width <= available-width { + return default + } + + // If there is not enough horizontal space, use multiple lines. + + let line-builder = stack.with( + dir: ltr, + spacing: min-spacing, + ) + + let lines = ((), ) + for premise in premises { + let augmented-line = lines.last() + (premise, ) + if available-width == none or measure(line-builder(..augmented-line)).width <= available-width { + lines.last() = augmented-line + } else { + lines.push((premise, )) + } + } + + layout-content({ + set align(center) + stack( + dir: ttb, + spacing: 0.7em, + ..lines + .filter(line => line.len() != 0) + .map(line => line-builder(..line)), + ) + }) + } + + + /// Lays out the horizontal bar of a rule. + let layout-bar( + /// The stroke to use for the bar. + stroke, + /// The length of the bar, without taking hangs into account. + length, + /// How much to extend the bar to the left and to the right. + hang, + /// The label of the rule, displayed on the left of the bar. + /// + /// If this is `none`, no label is displayed. + label, + /// The name of the rule, displayed on the right of the bar. + /// + /// If this is `none`, no name is displayed. + name, + /// The space to leave between the label and the bar, and between the bar + /// and the name. + margin, + /// The minimum height of the content to return. + min-height, + ) = { + let bar = line( + start: (0pt, 0pt), + length: length + 2 * hang, + stroke: stroke, + ) + + let (width: label-width, height: label-height) = measure(label) + let (width: name-width, height: name-height) = measure(name) + + let content = { + show: box.with( + // stroke: green + 0.3pt, // DEBUG + height: calc.max(label-height, name-height, min-height), + ) + + set align(horizon) + + let bake(body) = if body == none { + none + } else { + move(dy: -0.15em, box(body, ..measure(body))) + } + + let parts = ( + bake(label), + bar, + bake(name), + ).filter(p => p != none) + + stack( + dir: ltr, + spacing: margin, + ..parts, + ) + } + + ( + content: content, + left-blank: + if label == none { + hang + } else { + hang + margin + label-width + }, + right-blank: + if name == none { + hang + } else { + hang + margin + name-width + }, + ) + } + + + /// Lays out the application of a rule. + let layout-rule( + /// The laid out premises. + /// + /// This must be a dictionary with `content`, `left-blank` + /// and `right-blank` attributes. + premises, + /// The conclusion, displayed below the bar. + conclusion, + /// The stroke of the bar. + bar-stroke, + /// The amount by which to extend the bar on each side. + bar-hang, + /// The label of the rule, displayed on the left of the bar. + /// + /// If this is `none`, no label is displayed. + label, + /// The name of the rule, displayed on the right of the bar. + /// + /// If this is `none`, no name is displayed. + name, + /// The space to leave between the label and the bar, and between the bar + /// and the name. + bar-margin, + /// The spacing above and below the bar. + horizontal-spacing, + /// The minimum height of the bar element. + min-bar-height, + ) = { + // Fix the dimensions of the conclusion and name to prevent problems with + // fractional units later. + conclusion = box(conclusion, ..measure(conclusion)) + + let premises-inner-width = measure(premises.content).width - premises.left-blank - premises.right-blank + let conclusion-width = measure(conclusion).width + + let bar-length = calc.max(premises-inner-width, conclusion-width) + + let bar = layout-bar(bar-stroke, bar-length, bar-hang, label, name, bar-margin, min-bar-height) + + let left-start + let right-start + + let premises-left-offset + let conclusion-left-offset + + if premises-inner-width > conclusion-width { + left-start = calc.max(premises.left-blank, bar.left-blank) + right-start = calc.max(premises.right-blank, bar.right-blank) + premises-left-offset = left-start - premises.left-blank + conclusion-left-offset = left-start + (premises-inner-width - conclusion-width) / 2 + } else { + let premises-left-hang = premises.left-blank - (bar-length - premises-inner-width) / 2 + let premises-right-hang = premises.right-blank - (bar-length - premises-inner-width) / 2 + left-start = calc.max(premises-left-hang, bar.left-blank) + right-start = calc.max(premises-right-hang, bar.right-blank) + premises-left-offset = left-start + (bar-length - premises-inner-width) / 2 - premises.left-blank + conclusion-left-offset = left-start + } + let bar-left-offset = left-start - bar.left-blank + + let content = { + // show: box.with(stroke: yellow + 0.3pt) // DEBUG + + let stack-dir = dir.inv() + let align-y = dir.start() + + set align(align-y + left) + + stack( + dir: stack-dir, + spacing: horizontal-spacing, + h(premises-left-offset) + premises.content, + h(bar-left-offset) + bar.content, + h(conclusion-left-offset) + conclusion, + ) + } + + ( + content: box(content), + left-blank: left-start + (bar-length - conclusion-width) / 2, + right-blank: right-start + (bar-length - conclusion-width) / 2, + ) + } + + + /// Lays out an entire proof tree. + /// + /// All lengths passed to this function must be resolved. + let layout-tree( + /// The rule containing the tree to lay out. + rule, + /// The available width for the tree. + /// + /// `none` is interpreted as infinite available width. + /// + /// Ideally, the width of the returned tree should be bounded by this value, + /// although no guarantee is made. + available-width, + /// The minimum amount between each premise. + min-premise-spacing, + /// The stroke of the bar. + bar-stroke, + /// The amount by which to extend the bar on each side. + bar-hang, + /// The space to leave between the label and the bar, and between the bar + /// and the name. + bar-margin, + /// The margin above and below the bar. + horizontal-spacing, + /// The minimum height of the bar element. + min-bar-height, + ) = { + if type(rule) != dictionary { + return layout-content(rule) + } + + // A small branch is a tree whose premises (if any) are all leaves. The + // premises of such a tree can be typeset in multiple lines in case there is + // not enough horizontal space. + let is-small-branch = rule.premises.all(premise => type(premise) != dictionary) + let premises = if is-small-branch { + let width-available-to-premises = none + if available-width != none { + width-available-to-premises = available-width - bar-hang * 2 + if rule.name != none { + width-available-to-premises -= bar-margin + measure(rule.name).width + } + if rule.label != none { + width-available-to-premises -= bar-margin + measure(rule.label).width + } + // This fixes some rounding issues in auto sized containers. + width-available-to-premises += 0.00000001pt + } + layout-leaf-premises( + rule.premises, + min-premise-spacing, + measure(rule.conclusion).width, + width-available-to-premises, + ) + } else { + layout-premises( + rule.premises.map(premise => layout-tree( + premise, + none, + min-premise-spacing, + bar-stroke, + bar-hang, + bar-margin, + horizontal-spacing, + min-bar-height, + )), + min-premise-spacing, + measure(rule.conclusion).width, + ) + } + + layout-rule( + premises, + rule.conclusion, + bar-stroke, + bar-hang, + rule.label, + rule.name, + bar-margin, + horizontal-spacing, + min-bar-height, + ) + } + + + layout(available => { + let tree = layout-tree( + rule, + available.width, + prem-min-spacing.to-absolute(), + stroke, + title-inset.to-absolute(), + title-inset.to-absolute(), + horizontal-spacing.to-absolute(), + min-bar-height.to-absolute(), + ).content + + block( + // stroke : black + 0.3pt, // DEBUG + ..measure(tree), + breakable: false, + tree, + ) + }) +} diff --git a/packages/preview/curryst/0.4.0/examples/math-formula.svg b/packages/preview/curryst/0.4.0/examples/math-formula.svg new file mode 100644 index 000000000..bb80365d7 --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/math-formula.svg @@ -0,0 +1,258 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/packages/preview/curryst/0.4.0/examples/math-formula.typ b/packages/preview/curryst/0.4.0/examples/math-formula.typ new file mode 100644 index 000000000..598b6a8a6 --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/math-formula.typ @@ -0,0 +1,15 @@ +#import "../curryst.typ": rule, proof-tree +#set document(date: none) +#set page(width: auto, height: auto, margin: 0.5cm, fill: white) + +Consider the following tree: +$ + Pi quad = quad #proof-tree( + rule( + $phi$, + $Pi_1$, + $Pi_2$, + ) + ) +$ +$Pi$ constitutes a derivation of $phi$. diff --git a/packages/preview/curryst/0.4.0/examples/natural-deduction.svg b/packages/preview/curryst/0.4.0/examples/natural-deduction.svg new file mode 100644 index 000000000..b467cd597 --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/natural-deduction.svg @@ -0,0 +1,927 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/packages/preview/curryst/0.4.0/examples/natural-deduction.typ b/packages/preview/curryst/0.4.0/examples/natural-deduction.typ new file mode 100644 index 000000000..de4615415 --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/natural-deduction.typ @@ -0,0 +1,35 @@ +#import "../curryst.typ": rule, proof-tree +#set document(date: none) +#set page(width: auto, height: auto, margin: 0.5cm, fill: white) + +#let ax = rule.with(name: [ax]) +#let and-el = rule.with(name: $and_e^ell$) +#let and-er = rule.with(name: $and_e^r$) +#let impl-i = rule.with(name: $scripts(->)_i$) +#let impl-e = rule.with(name: $scripts(->)_e$) +#let not-i = rule.with(name: $not_i$) +#let not-e = rule.with(name: $not_e$) + +#proof-tree( + impl-i( + $tack (p -> q) -> not (p and not q)$, + not-i( + $p -> q tack not (p and not q)$, + not-e( + $ underbrace(p -> q\, p and not q, Gamma) tack bot $, + impl-e( + $Gamma tack q$, + ax($Gamma tack p -> q$), + and-el( + $Gamma tack p$, + ax($Gamma tack p and not q$), + ), + ), + and-er( + $Gamma tack not q$, + ax($Gamma tack p and not q$), + ), + ), + ), + ) +) diff --git a/packages/preview/curryst/0.4.0/examples/rule-as-premise.svg b/packages/preview/curryst/0.4.0/examples/rule-as-premise.svg new file mode 100644 index 000000000..aabc7e75a --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/rule-as-premise.svg @@ -0,0 +1,368 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/packages/preview/curryst/0.4.0/examples/rule-as-premise.typ b/packages/preview/curryst/0.4.0/examples/rule-as-premise.typ new file mode 100644 index 000000000..be4d9c3dc --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/rule-as-premise.typ @@ -0,0 +1,22 @@ +#import "../curryst.typ": rule, proof-tree +#set document(date: none) +#set page(width: auto, height: auto, margin: 0.5cm, fill: white) + +#proof-tree( + rule( + name: $R$, + $C_1 or C_2 or C_3$, + rule( + name: $A$, + $C_1 or C_2 or L$, + rule( + $C_1 or L$, + $Pi_1$, + ), + ), + rule( + $C_2 or overline(L)$, + $Pi_2$, + ), + ) +) diff --git a/packages/preview/curryst/0.4.0/examples/usage.svg b/packages/preview/curryst/0.4.0/examples/usage.svg new file mode 100644 index 000000000..b8989d45a --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/usage.svg @@ -0,0 +1,216 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/packages/preview/curryst/0.4.0/examples/usage.typ b/packages/preview/curryst/0.4.0/examples/usage.typ new file mode 100644 index 000000000..3937f04ad --- /dev/null +++ b/packages/preview/curryst/0.4.0/examples/usage.typ @@ -0,0 +1,14 @@ +#import "../curryst.typ": rule, proof-tree +#set document(date: none) +#set page(width: auto, height: auto, margin: 0.5cm, fill: white) + +#let tree = rule( + label: [Label], + name: [Rule name], + [Conclusion], + [Premise 1], + [Premise 2], + [Premise 3] +) + +#proof-tree(tree) diff --git a/packages/preview/curryst/0.4.0/typst.toml b/packages/preview/curryst/0.4.0/typst.toml new file mode 100644 index 000000000..a008a0f14 --- /dev/null +++ b/packages/preview/curryst/0.4.0/typst.toml @@ -0,0 +1,13 @@ +[package] +name = "curryst" +version = "0.4.0" +entrypoint = "curryst.typ" +authors = ["Rémi Hutin <@remih23>", "Paul Adam <@pauladam94>", "Malo <@MDLC01>"] +license = "MIT" +description = "Typeset trees of inference rules." +repository = "https://github.com/pauladam94/curryst" +keywords = ["proof tree", "prooftree", "inference", "logic"] +categories = ["components", "visualization", "integration"] +disciplines = ["computer-science", "mathematics"] +compiler = "0.12.0" +exclude = [".gitignore", "examples/*", "tests/*"]