val string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t
let string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t =
  let open C.String in
  let open Spec.Agile.Hash in
  function
  | MD5 -> !$"MD5"
  | SHA1 -> !$"SHA1"
  | SHA2_224 -> !$"SHA2_224"
  | SHA2_256 -> !$"SHA2_256"
  | SHA2_384 -> !$"SHA2_384"
  | SHA2_512 -> !$"SHA2_512"
  | SHA3_224 -> !$"SHA3_224"
  | SHA3_256 -> !$"SHA3_256"
  | SHA3_384 -> !$"SHA3_384"
  | SHA3_512 -> !$"SHA3_512"
  | Blake2S -> !$"Blake2S"
  | Blake2B -> !$"Blake2B"
  | Shake128 -> !$"Shake128"
  | Shake256 -> !$"Shake256"
val string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t
let string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t =
let open C.String in
let open Spec.Agile.Hash in
function
| MD5 -> !$"MD5"
| SHA1 -> !$"SHA1"
| SHA2_224 -> !$"SHA2_224"
| SHA2_256 -> !$"SHA2_256"
| SHA2_384 -> !$"SHA2_384"
| SHA2_512 -> !$"SHA2_512"
| SHA3_224 -> !$"SHA3_224"
| SHA3_256 -> !$"SHA3_256"
| SHA3_384 -> !$"SHA3_384"
| SHA3_512 -> !$"SHA3_512"
| Blake2S -> !$"Blake2S"
| Blake2B -> !$"Blake2B"
| Shake128 -> !$"Shake128"
| Shake256 -> !$"Shake256"
Test.NoHeap.fst.checked
TestLib.fsti.checked Test.Vectors.Poly1305.fst.checked Test.Vectors.Curve25519.fst.checked Test.Vectors.Chacha20Poly1305.fst.checked Test.Vectors.fst.checked Test.Lowstarize.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked LowStar.Failure.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Poly1305.fsti.checked EverCrypt.HMAC.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Hash.Incremental.fst.checked EverCrypt.Hash.fsti.checked EverCrypt.Curve25519.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.Chacha20Poly1305.fsti.checked C.String.fsti.checked C.Loops.fst.checked
Test.NoHeap.fst
Spec.Hash.Definitions.hash_alg C.String.op_Bang_Dollar C.String.t
module Test.NoHeap

module B = LowStar.Buffer
module L = Test.Lowstarize
module U32 = FStar.UInt32

open FStar.HyperStack.ST
open FStar.Integers
open LowStar.BufferOps
open Test.Lowstarize

let string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t =
  let open C.String in
val string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t
_: Spec.Hash.Definitions.hash_alg -> C.String.t