Crate unbound 

Locally nameless representation for capture-avoiding substitution and alpha equivalence in Rust.

• Name types for representing variables with globally unique identifiers
• Bind types for representing binding constructs (like lambda abstractions)
• Automatic alpha equivalence via the Alpha trait (derivable)
• Capture-avoiding substitution via the Subst trait (derivable)
• Fresh name generation via the FreshM monad

Quick Start

use unbound::prelude::*;

#[derive(Clone, Debug, Alpha, Subst)]
enum Expr {
    Var(Name<Expr>),
    Lam(Bind<Name<Expr>, Box<Expr>>),
    App(Box<Expr>, Box<Expr>),
}

Re-exports

pub use alpha::Alpha;

pub use alpha::AlphaCtx;

Modules

alpha

Alpha equivalence for terms with binding

prelude

A prelude module that re-exports commonly used items

Structs

Bind

A binding construct that binds a name within a term

FreshM

The Fresh monad for generating fresh names

FreshState

State for fresh name generation

Name

A name with a phantom type parameter

Enums

SubstName

A wrapper type for names used in substitution

Traits

Fresh

Trait for types that can provide fresh names

Subst

Trait for types that support substitution

Functions

bind

Helper function to bind a pattern in a body

run_fresh

Helper to run a FreshM computation

s2n

Helper function to create a name from a string

Derive Macros

Alpha

Derive macro for the Alpha trait

Subst

Derive macro for the Subst trait