proofs.rs

Trait method

<T as num_conv::Widen>::widen

impl<T: sealed::Integer> num_conv::Widen for T
pub fn widen<U>(self: Self) -> U where T: WidenTarget<U>

Documentation on docs.rs

Claims (1)

Claim #1 — Verification of <T as num_conv::Widen>::widen (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)
<T as num_conv::Widen>::widen

num-conv 0.2.2 integer conversion correctness · v1 · 0 comments · MasWag