Crate mononym

Mononym is a library for creating unique type-level names for each value in Rust. The core type Named<Name, T> represents a named value of type T with a unique type Name as its name. Mononym guarantees that there can be no two values with the same name. With that, the Name type serves as a unique representation of a Rust value at the type level.

Mononym enables the use of the design pattern Ghosts of Departed Proofs in Rust. It provides macros that simplify the definition of dependent pairs and proof objects in Rust. Although there is still limited support for a full dependently-typed programming in Rust, Mononym helps us move a small step toward that direction by making it possible to refer to values in types.

See docs::implementation for how mononym implements unique name generation in Rust.

Re-exports

pub use named::with_seed;

pub use named::HasType;

pub use named::Life;

pub use named::Name;

pub use named::Named;

pub use named::Seed;

Modules

docs

This is a rustdoc-only module providing in depth documentation on the library.

named

The main implementation for named data types.

proof

Macros

exists

Macro to define new named value coupled with proofs in the form of dependent pairs.

exists_single

proof

Macro to help define a new proof type.

proof_single