type Observation

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:439

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

439# Reify an affine owner once for proof consumers that need both its Data model
440# and the relation. This helper is never imported by a numerical runtime path.
441type Observation<-Element: Data,-storage: Array<Element>> is Data:
442  Observation{tree: Tree.Tree<Element>,packed: {Tree.pack(Element,tree) == storage : Array<Element>},
443    reflected: {tree == Tree.reflect(Element,storage) : Tree.Tree<Element>}}