Crate lolli_viz 

lolli-viz

Visualization for the Lolli linear logic workbench.

This crate provides rendering of proofs as trees, LaTeX, and graphs.

Output Formats

• ASCII/Unicode: Terminal-friendly proof trees
• LaTeX: Using bussproofs package
• DOT: Graphviz format for graph visualization

Example

use lolli_viz::{TreeRenderer, render_ascii};
use lolli_core::{Formula, Proof, Rule, Sequent};

let proof = Proof {
    conclusion: Sequent::new(vec![Formula::neg_atom("A"), Formula::atom("A")]),
    rule: Rule::Axiom,
    premises: vec![],
};

let ascii = render_ascii(&proof);
println!("{}", ascii);

Structs

DotRenderer

Graphviz DOT renderer for proofs.

LatexRenderer

LaTeX proof renderer using bussproofs package.

Proof

A proof in the sequent calculus.

Sequent

A one-sided sequent ⊢ Γ.

TreeRenderer

Proof tree renderer for ASCII/Unicode output.

Enums

Formula

A linear logic formula.

Rule

Inference rules for linear logic sequent calculus.

Functions

render_ascii

Render a proof as ASCII text.

render_dot

Render a proof as Graphviz DOT format.

render_latex

Render a proof as LaTeX (bussproofs package).

render_unicode

Render a proof as Unicode text (with box-drawing characters).