Struct ModuleInfo 

pub struct ModuleInfo {
    pub prefix: String,
    pub depends: Vec<String>,
    pub type_defs: Vec<TypeDef>,
    pub fn_defs: Vec<FnDef>,
    pub verify_laws: Vec<VerifyBlock>,
    pub analysis: Option<AnalysisResult>,
}

Information about a dependent module loaded for codegen.

Fields

prefix: String

Qualified module path, e.g. “Models.User”.

depends: Vec<String>

Direct depends [...] entries from the source module.

type_defs: Vec<TypeDef>

Type definitions from the module.

fn_defs: Vec<FnDef>

Function definitions from the module (excluding main).

verify_laws: Vec<VerifyBlock>

verify … law blocks of this dep module, in source order.

Carried so the Lean proof backend can (a) emit each proven dep law as a <fn>_law_<name> theorem inside namespace M, and (b) admit it into a consumer law’s lemma pool under the same cone ∪ subject admissibility gate as in-file sibling laws — the cross-file law pool. Only VerifyKind::Law blocks are kept; plain example-style verify blocks in a dep are still dropped (module-scoped sampling is a separate feature). Read ONLY by the Lean proof emit / pool; inert for every other backend.

analysis: Option<AnalysisResult>

IR-level analysis facts produced by the dep module’s pipeline run (analyze stage). None for modules loaded via paths that skip the analyze stage (none in production today; left optional for future ad-hoc loaders). Aver’s module DAG invariant makes per-module analysis sufficient — see project_aver_module_dag memory and src/ir/analyze.rs for why cross-module SCCs are impossible.

Implementations

impl ModuleInfo

pub fn from_loaded(loaded: &LoadedModule) -> Self

Build a ModuleInfo from a freshly-parsed LoadedModule. Skips the analyze stage — callers that need per-dep analysis facts should run the pipeline themselves (see crate::main::commands::load_compile_deps / playground::loaded_to_module_info). Used by ad-hoc loaders (vm_profile, the eval-spec test helpers) that just need the dep’s symbol layout to feed SymbolTable::build / pipeline::run’s dep_modules slot.