val legacy_update_multi: update_multi_st (|MD5, ()|)
let legacy_update_multi: update_multi_st (|MD5, ()|) =
  Hacl.Hash.MD.mk_update_multi MD5 legacy_update
val legacy_update_multi: update_multi_st (|MD5, ()|)
let legacy_update_multi:update_multi_st (| MD5, () |) =
Hacl.Hash.MD.mk_update_multi MD5 legacy_update
Hacl.Hash.MD5.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Hacl.Hash.MD.fst.checked Hacl.Hash.Definitions.fst.checked Hacl.Hash.Core.MD5.fsti.checked FStar.Pervasives.fsti.checked
Hacl.Hash.MD5.fst
Hacl.Hash.MD.mk_update_multi Spec.Hash.Definitions.MD5 Hacl.Hash.Core.MD5.legacy_update Hacl.Hash.Definitions.update_multi_st Prims.Mkdtuple2 Spec.Hash.Definitions.hash_alg Hacl.Hash.Definitions.m_spec
module Hacl.Hash.MD5

open Hacl.Hash.Definitions
open Spec.Hash.Definitions

include Hacl.Hash.Core.MD5

friend Hacl.Hash.MD
val legacy_update_multi: update_multi_st (|MD5, ()|)
Hacl.Hash.Definitions.update_multi_st (| Spec.Hash.Definitions.MD5, () |)