Type Alias EverCrypt_Hash_alg 

pub type EverCrypt_Hash_alg = Spec_Hash_Definitions_hash_alg;