Module display 

Rendering of contracts, function signatures, and verification results.

Presentation-only helpers: contract expansion to (call, meaning) pairs, function paths with generic bounds, and grouped result trees with verdicts.

Functions

dedup_compound_props 🔒

Drop consecutive duplicate compound-def entries: a def expands to several primitives sharing the same origin name and arguments, which should render as a single name(args) line.

emit_property_rows 🔒

emit_results_and_verdict 🔒

emit_results_counts_and_checkpoints 🔒

emit_verify_summary 🔒

fmt_contract_expanded 🔒

fmt_fn_path_with_bounds 🔒

fmt_fn_path_with_generics 🔒

fmt_fn_with_params 🔒

fmt_index_access 🔒

Render an IndexAccess { slice, index } into (slice_str, index_str), stripping leading &mut /& from the slice display.

fmt_meaning_template 🔒

Substitute {0}, {1}, {2} placeholders in a meaning template with the rendered positional arguments. Missing arguments fall back to "_".

insert_bounds_into_path 🔒