def ready_observed

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:115

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage

115def ready_observed(~Element: Data,-buffer: Storage.Buffer<Element>,+model: Model<Element>,equation: {pack(~Element,model) == buffer : Storage.Buffer<Element>},
116  ready: NativeReady(~Element,buffer)) -> Sized<Element,model>:
117  ready_packed(~Element,model,
118    %Equal.sym(Storage.Buffer<Element>,pack(~Element,model),buffer,equation) : NativeReady(~Element,_) ready)