TraversalLanesRefinement.output: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement
Lines 148-152 of stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&start_line=148&end_line=152

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Batch
import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws
import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as MapReadback
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

# The scalar map from any position, on a packed tree.
def output(~Context: Data,+state: Batch.ModelState(~F32,~Context)) ->
  {Traversal.mapped_output(~F32,~Context,ArrayLaws.represent_map(~F32,~Context,state)) == Tree.pack(F32,MapReadback.output(~F32,~Context,state)) : Array<F32>}:
  Traversal.State{Unit{},output,position,context} = state
  {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=represent_map
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=ModelState
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=output
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=mapped_output