Function diagnostics 

pub fn diagnostics(
    imported: &ImportedContext,
    target: &str,
    target_lean: &str,
    assumptions: &[String],
) -> Vec<Diagnostic>

One disallowed_assumption diagnostic of the assumption-policy stage per assumption outside Lean’s three standard axioms that target (a kernel name, printed as target_lean) rests on, naming its taint path. assumptions are the result’s (Lean names).