Function import 

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

Import the export and return its checked context: no audit, nothing retained, Lean’s binder names carried.