sequent-md renders keyboard-friendly sequent-calculus Markdown fences as
conventional proof trees. It targets VS Code Markdown Preview and
remark/rehype-based HTML pipelines.
Write a sequent fence. The premises sit above the deduction bar and the
conclusion below it:
And-Intro :=
[ GAMMA |- A ] [ GAMMA |- B ]
===>
GAMMA |- A /\ B
It renders as a rule named And-Intro, with Γ ⊢ A and Γ ⊢ B as sibling
premises and Γ ⊢ A ∧ B as its conclusion.
Use the core renderer wherever you need an HTML fragment. It returns the parsed tree and diagnostics alongside the HTML.
import {render} from '@sequent-md/core';
const {html, diagnostics} = render(source);Add the rehype plugin to a Unified pipeline. It replaces fenced
language-sequent code blocks with semantic proof-tree HAST.
import {rehypeSequent} from '@sequent-md/rehype';
processor.use(rehypeSequent);Use the separate Node exporter to create a standalone image with outlined glyphs. The bundled fonts make the image independent of reader fonts.
import {writeFile} from 'node:fs/promises';
import {renderSvg} from '@sequent-md/core/svg';
const result = await renderSvg(source, {
maxWidth: 320,
title: 'Conjunction introduction',
description: 'Two premises establish a conjunction.'
});
if (result.diagnostics.length) throw new Error(JSON.stringify(result.diagnostics));
await writeFile('proof.svg', result.svg);The exporter retains the parsed tree, canonical source, and diagnostic behavior. It wraps formula text at whitespace and packs premises into rows to target the requested width. Explicit continuation breaks and hanging indentation remain visible. Unbreakable tokens or long labels can require a wider image.
See SVG export for options, custom fonts, and accessibility, and format verification for HTML, EPUB, and Typst PDF checks. HTML previews keep their existing layout.
Build and package the included extension, then install the resulting VSIX:
npm run build
(cd packages/vscode && npx --yes @vscode/vsce package --no-dependencies --out sequent-md-vscode.vsix)
code --install-extension packages/vscode/sequent-md-vscode.vsix --forceOpen a Markdown preview containing a sequent fence. The extension supplies
both the renderer and its stylesheet.
- A named
6DBC
rule starts with
Name :=orName ::=, followed by an indented proof. Implemented names start with a letter or underscore, then may contain letters, digits, underscores, and hyphens.=>and===>both introduce the conclusion. - A deduction operator can appear first, creating a zero-premise rule (an axiom).
- Bracketed derivations nest:
[ ... ]. Adjacent bracket groups such as[ GAMMA |- A ] [ GAMMA |- B ]are sibling premises. family name:groups related named rules into a responsive visual family.- Formulae accept Unicode or typing-friendly notation: aliases such as
|-,->,/\,\/,forall,box,next,tensor, and-*, plus the linear-logic marker!. The ordinary characters+,-,*,/, and|are formula text; only registered compound aliases are rewritten.
Pass a symbols map to the core renderer or rehype plugin to add aliases or
override the defaults. Custom entries are merged with the built-in logical,
Greek, modal, temporal, and linear-logic vocabulary.
Uppercase environment aliases include OMEGA → Ω, XI → Ξ, IOTA → Ι,
PHI → Φ, and MU → Μ. They are case-sensitive and use whole-word matching:
OMEGA_value and prefixOMEGA remain literal identifiers.
Environment-Notation :=
===>
GAMMA; DELTA; OMEGA; XI; IOTA; PHI; MU |- expression ⇒ type
The conclusion displays Γ; Δ; Ω; Ξ; Ι; Φ; Μ ⊢ expression ⇒ type with defaults,
including in VS Code preview and native SVG export. The explicit mapping below
also works, although these five entries are already defaults:
render(source, {symbols: {
OMEGA: 'Ω', XI: 'Ξ', IOTA: 'Ι', PHI: 'Φ', MU: 'Μ'
}});Caller entries take precedence: {symbols: {OMEGA: 'ω'}} changes that alias to
lowercase ω while retaining the other defaults.
const symbols = {
judgement: '⊨',
square: '□'
};
render(source, {symbols});
processor.use(rehypeSequent, {symbols});Word aliases match complete words, so an alias such as lambda does not alter
lambdaValue. Structural syntax (:=, =>, and brackets) is not configurable.
The included VS Code adapter currently uses the default symbol vocabulary.
- Guide: how to read and write sequents, with worked examples.
- Grammar: the implemented grammar and its EBNF reference.
- Examples: Identity, Nested derivation, Classical logic, and Intuitionistic linear logic.
Run npm test for the parser, renderer, documentation, and adapter suites.
Run npm run build to bundle the VS Code extension and generate its preview
stylesheet.