Function ieee_float_cast Copy item path

pub open spec fn ieee_float_cast<From: IeeeFloatCast<To>, To>(from: From) -> To

{ from.ieee_cast() }