Merckle Tree on Coq https://github.com/FStarLang/FStar/blob/da2667abaa1debfbab714acb678f68f71dab25e3/examples/data_structures/MerkleTree.fst Requirement Coq (version 8.10) Build ./configure.sh make Coqdoc Documents https://proof-ninja.co.jp/merckletree_coq/