Struct EnvBuilder 

pub struct EnvBuilder { /* private fields */ }

A thin wrapper around Environment providing convenience methods for registering axioms and definitions during standard library initialisation.

Implementations

impl EnvBuilder

pub fn new(env: Environment) -> Self

Create a new builder from an existing environment.

pub fn fresh() -> Self

Create a builder around a fresh Environment::new().

pub fn add_axiom(&mut self, name: Name, ty: Expr)

Add an axiom with the given name and type.

pub fn axiom(&mut self, name: &str, ty: Expr) -> &mut Self

Add an axiom using a &str name.

pub fn add_definition(&mut self, name: Name, ty: Expr, value: Expr)

Add a definition with the given name, type, and value.

pub fn def(&mut self, name: &str, ty: Expr, value: Expr) -> &mut Self

Add a definition using a &str name (builder-style).

pub fn theorem(&mut self, name: &str, ty: Expr, proof: Expr) -> &mut Self

Add a theorem (opaque definition) using a &str name.

pub fn sorry(&mut self, name: &str, ty: Expr) -> &mut Self

Add a Sorry opaque axiom — useful for placeholder proofs.

pub fn finish(self) -> Result<Environment, String>

Finish building and return the environment, or an error string.

pub fn finish_or_panic(self) -> Environment

Finish building, panicking on any error. Useful in tests.

pub fn env(&self) -> &Environment

Get a reference to the underlying environment.

pub fn is_ok(&self) -> bool

true if no errors have been accumulated.

pub fn errors(&self) -> &[String]

Return the accumulated error messages.

pub fn contains(&self, name: &str) -> bool

Check whether name has been registered.