let pt = fun _ _ _ -> True
let pt =
fun _ _ _ -> True
MerkleTree.fsti.checked
prims.fst.checked MerkleTree.Spec.fst.checked MerkleTree.Low.Serialization.fst.checked MerkleTree.Low.Hashfunctions.fst.checked MerkleTree.Low.Datastructures.fst.checked MerkleTree.Low.fst.checked MerkleTree.EverCrypt.fsti.checked LowStar.ConstBuffer.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
MerkleTree.fsti
Prims.l_True Prims.logical
module MerkleTree

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module HH = FStar.Monotonic.HyperHeap

module B = LowStar.Buffer
module CB = LowStar.ConstBuffer

module U32 = FStar.UInt32
module U64 = FStar.UInt64

module MTS = MerkleTree.Spec
module MTNL = MerkleTree.Low
module MTNLHF = MerkleTree.Low.Hashfunctions
module MTNLE = MerkleTree.EverCrypt
module MTNLD = MerkleTree.Low.Datastructures
module MTNLS = MerkleTree.Low.Serialization


let hash_size_t = MTNLD.hash_size_t
let offset_t = MTNL.offset_t
let index_t = MTNL.index_t
let hash #hash_size = MTNLD.hash #hash_size

type path = MTNL.path
type path_p = B.pointer path
type const_path_p = MTNL.const_pointer path

let merkle_tree = MTNL.merkle_tree
let mt_p = MTNL.mt_p
let const_mt_p = MTNL.const_mt_p

inline_for_extraction noextract
let pf = fun _ -> False
val pt : _: _ -> _: _ -> _: _ -> Prims.logical
_: _ -> _: _ -> _: _ -> Prims.logical