TraversalCellsRefinement.observe: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as TraversalCellsRefinement
Lines 57-59 of stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&start_line=57&end_line=59

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

def observe(~Owner: Type,~Model: Type,~Cell: Data,~Context: Data,~project: Owner -> Model,state: Cells.State<Owner,Cell,Context>) -> Observed<Model,Cell,Context>:
  Cells.State{values,scratch,position,slot,context} = state
  Observed{project(values),Tree.reflect(Cell,scratch),position,slot,context}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=reflect
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=Observed
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=State