Module lean_format

Structs§

def_id_to_pascal_case
impl_header_name 🔒
is_reserved 🔒
sanitize_name 🔒
snake_case_to_pascal_case
stable_def_path 🔒: 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.
stable_impl_name 🔒: A name for an impl block derived from its header: SelfTy_as_Trait for trait impls and SelfTy for inherent impls. In the rare case where several impls in the same parent get the same name, e.g., because their generic parameters are named differently, they are suffixed with their index among those impls.