def native_content_ready

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:104

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

104def native_content_ready(~Element: Data,buffer: Storage.Buffer<Element>,ready: NativeReady(~Element,buffer)) -> ContentReady<Element,contents(~Element,buffer)>:
105  Storage.Buffer{storage,length,Certificate.Certificate{+depth,equation}} = buffer
106  Shape.Both{depth_ok,room} = ready
107  ContentReady{depth,Witness.balanced(Element,depth,storage,Certificate.witness_at(Element,depth,storage,equation)),depth_ok,room}