def allocate

stelliferous@0.0.2.0 · storage_buffer.bend:9

import Base
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate

9# Construction records evidence once, without visiting the owner or carrying
10# certificates through the elementwise loop.
11def allocate(~Element: Data,+depth: Nat,+value: Element,length: Nat) -> Buffer<Element>:
12  Buffer{Array.new(Element,depth,value),length,Certificate.allocated(Element,depth,value)}