Skip to main content

decode_pod

ostd_pod

Function decode_pod 

Source 
pub open spec fn decode_pod<T: Pod>(bytes: Seq<u8>) -> T
Expand description
{ choose |v: T| pod_bytes::<T>(v) == bytes }

The Pod value whose byte representation equals bytes (when one exists).

Defined via choose over the injective pod_bytes; if no Pod value maps to bytes, the result is arbitrary. Callers should establish existence before relying on the returned value.