def observe
stelliferous@0.0.2.0 · proofs/storage_refinement.bend:466
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
466def observe(-Element: Data,storage: Array<Element>) -> Observation<Element,storage>:
467 match storage:
468 case ALeaf{+value}: Observation{Tree.Leaf{value},{==},{==}}
469 case ANode{left,right}: observed_node(Element,left,right,observe(Element,left),observe(Element,right))