Skip to main content

Module codegen

Module codegen 

Source

Modules§

common
dafny
lean
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.

Structs§

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.

Functions§

build_context
Build a CodegenContext from parsed + type-checked items.