lolli_core/lib.rs
1//! # lolli-core
2//!
3//! Core data structures for the Lolli linear logic workbench.
4//!
5//! Linear logic is a resource-aware logic where hypotheses must be used exactly once.
6//! This crate provides the fundamental types for working with linear logic formulas,
7//! sequents, proofs, and extracted terms.
8//!
9//! ## Linear Logic Connectives
10//!
11//! | Connective | Symbol | Name | Meaning |
12//! |------------|--------|------|---------|
13//! | Tensor | A ⊗ B | "times" | Both A and B (independently) |
14//! | Par | A ⅋ B | "par" | A or B (opponent chooses) |
15//! | Lolli | A ⊸ B | "lollipop" | Consume A, produce B |
16//! | With | A & B | "with" | Both available, choose one |
17//! | Plus | A ⊕ B | "plus" | One of them (I choose) |
18//! | Of course | !A | "bang" | Unlimited supply of A |
19//! | Why not | ?A | "whynot" | Demand for A |
20
21#![warn(missing_docs)]
22#![warn(clippy::all)]
23
24pub mod formula;
25pub mod proof;
26pub mod sequent;
27pub mod term;
28
29pub use formula::Formula;
30pub use proof::{Proof, Rule};
31pub use sequent::{Sequent, TwoSidedSequent};
32pub use term::Term;