Skip to main content

Module basic

Module basic 

Source
Expand description

Lightweight import-parity module for Lean’s CommerceTheory.Basic.

Domain declarations live in the focused Rust modules re-exported from lib.rs; this module exists so the Rust crate has the same top-level shape as the updated Lean package.

Constants§

BASIC_MODULE_LOADED