let lbytes (l:nat) = b:bytes {Seq.length b = l}
let lbytes (l: nat) =
b: bytes{Seq.length b = l}
Spec.Agile.HMAC.fsti.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Spec.Agile.HMAC.fsti
Prims.nat Spec.Hash.Definitions.bytes Prims.b2t Prims.op_Equality FStar.Seq.Base.length Lib.IntTypes.uint8
module Spec.Agile.HMAC

open Spec.Hash.Definitions
open Lib.IntTypes

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"
val lbytes : l: Prims.nat -> Type0
l: Prims.nat -> Type0