Function stable_def_path 

fn stable_def_path(tcx: TyCtxt<'_>, def_id: DefId) -> String

Like [rustc_hir::definitions::DefPath::to_filename_friendly_no_crate], but names impl blocks by their header (e.g., RawValIter_T_as_Iterator) instead of by their position in the enclosing module ({impl#10}). Lean names, and hence the names of user proof files, then stay the same when impl blocks are added, removed or reordered.

Components that would otherwise not be valid in a Lean identifier are rendered as follows:

• A const _ (e.g., the one defs! expands to, which declares flux items) is dropped if it is the first const _ in its parent, and rendered as _n for the n-th one after that, so items declared by the first (usually the only) defs! keep the name of the enclosing item.
• An anonymous component (e.g., {closure#0}) is rendered as closure_0.