def fresh

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:125

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

125def fresh(~Element: Data,+depth: Nat,+fill: Element,length: Nat) -> Model<Element>:
126  Model{Tree.fresh(Element,depth,fill),length,fresh_certificate(~Element,depth,fill)}