Crate lolli_parse 

lolli-parse

Parser for the Lolli linear logic workbench.

This crate provides parsing functionality for linear logic formulas and sequents.

Supported Syntax

Connective	Unicode	ASCII
Tensor	⊗	*
Par	⅋	`
Lolli	⊸	-o
With	&	&
Plus	⊕	+
Bang	!	!
Why not	?	?
Negation	A⊥	A^
Turnstile	⊢	|-

Example

use lolli_parse::{parse_formula, parse_sequent};

let formula = parse_formula("A -o B").unwrap();
assert_eq!(formula.pretty(), "(A ⊸ B)");

let sequent = parse_sequent("A, B |- A * B").unwrap();
assert_eq!(sequent.antecedent.len(), 2);

Structs

Sequent

A one-sided sequent ⊢ Γ.

TwoSidedSequent

A two-sided sequent Γ ⊢ Δ (for user-facing API).

Enums

Formula

A linear logic formula.

ParseError

Parse error type.

Rule

Functions

parse_formula

Parse a formula from a string.

parse_sequent

Parse a sequent from a string.