val ha : Type0
let ha = a:EverCrypt.HMAC.supported_alg{Spec.Hash.Definitions.is_md a}
module MiTLS.HMAC

open MiTLS.Hashing.Spec // for the algorithm names, instead of CoreCrypt
open MiTLS.Mem

open FStar.HyperStack.ST
/
Spec.Hash.Definitions.fst.checked prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked EverCrypt.HMAC.fsti.checked
MiTLS.HMAC.fsti
Type0
EverCrypt.HMAC.supported_alg Prims.b2t Spec.Hash.Definitions.is_md
let ha =
  
a: EverCrypt.HMAC.supported_alg{Spec.Hash.Definitions.is_md a}