vstd::function

Function proof_fn_as_req_ens

Source 
pub proof fn proof_fn_as_req_ens<R: ProofFnReqEnsDef<Args, Output>, const USAGE: u8, ReqEns, const COPY: u8, const SEND: u8, const SYNC: u8, ArgModes, OutMode, Args: Tuple, Output>(tracked 
    f: FnProof<'_, FOpts<USAGE, ReqEns, COPY, SEND, SYNC>, ArgModes, OutMode, Args, Output>,
) -> tracked FnProof<'_, FOpts<USAGE, RqEn<R>, COPY, SEND, SYNC>, ArgModes, OutMode, Args, Output>
Expand description
requires
forall |args: Args| #[trigger] R::req(args) ==> f.requires(args),
forall |args: Args, output: Output| {
    f.ensures(args, output) ==> #[trigger] R::ens(args, output)
},

Retype a proof_fn, introducing ReqEns