def output

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:148

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

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