Skip to main content

axiom_fmt_req_all_pointer

Function axiom_fmt_req_all_pointer 

Source
pub broadcast proof fn axiom_fmt_req_all_pointer<A: Pointer>(a: &A, f: &Formatter<'_>)
Expand description
requires
fmt_req_all::<A>(),
ensures
#[trigger] a.fmt_req(f),