def proposition

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:141

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate

141def proposition(~Element: Data,length: Nat,-storage: Array<Element>,-tree: Tree.Tree<Element>) -> Type:
142  @certificate: Certificate.Certificate<Element,storage> -> Observation<Element,Storage.Buffer{storage,length,certificate}>