Function extract_programs 

pub fn extract_programs(
    ctx: &Context,
    entries: &[&str],
) -> Result<String, ExtractError>

Extract a program rooted at several entry points into one Rust module.

Returns Rust source code as a string. The transitive dependencies of every entry are unioned, topologically sorted once, and emitted through a single [CodeGen], so shared dependencies (e.g. a Nat enum used by both add and double) are emitted exactly once.

Arguments

• ctx - The kernel context containing definitions and inductives
• entries - The names of the entry points to extract

Errors

Returns an error if any entry point is not found or cannot be extracted.