def observe

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:144

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws

144def observe(~Element: Data,buffer: Storage.Buffer<Element>) -> Observation<Element,buffer>:
145  Storage.Buffer{storage,+length,certificate} = buffer
146  StorageLaws.lift_observation(~Element,~Nat,~proposition(~Element),length,storage,StorageLaws.observe(Element,storage),
147    tree => certificate => Observation{Model{tree,length,certificate},{==}})(certificate)