Skip to main content Module codegen Copy item path Source common dafny lean lemma_discovery Committed-lemma consumption — the proof-side “sink” for auxiliary helper
lemmas. program_view Canonical resolved view of the program for codegen consumers. proof_lower Build ProofIR from a CodegenContext. recursion Shared proof-mode recursion analysis. rust scc Bare-name → FnId projection helpers for codegen boundary code. CodegenContext Collected context from the Aver program, shared across all backends. ModuleInfo Information about a dependent module loaded for codegen. ProjectOutput Output files from a codegen backend. build_context Build a CodegenContext from parsed + type-checked items. collect_verify_laws verify … law blocks from a module’s top-level items, in source
order. Plain example-style verify blocks (VerifyKind::Example)
are excluded — only laws are lifted into a dep’s ModuleInfo