StorageBufferModel.fresh: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as StorageBufferModel
Lines 125-126 of stelliferous@0.0.2.0/proofs/storage_buffer_model.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&start_line=125&end_line=126

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

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

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=Model
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_buffer_model.bend&name=fresh_certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=fresh