StorageRefinement.observe: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 466-469 of stelliferous@0.0.2.0/proofs/storage_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&start_line=466&end_line=469

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

def observe(-Element: Data,storage: Array<Element>) -> Observation<Element,storage>:
  match storage:
    case ALeaf{+value}: Observation{Tree.Leaf{value},{==},{==}}
    case ANode{left,right}: observed_node(Element,left,right,observe(Element,left),observe(Element,right))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=Observation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=observed_node
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree