Function import_audited_retaining_source 

pub fn import_audited_retaining_source(
    input: &str,
    name: &str,
) -> Result<(ImportedContext, ImportReport), Verdict>

Import and additionally retain the checked type and body of one named declaration, including an opaque theorem’s proof. Only that declaration is copied; every other import retains nothing extra.