TraversalLanesWitness.gather: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as TraversalLanesWitness
Lines 44-55 of stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&start_line=44&end_line=55

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

def gather(~Context: Data,~map: Context -> F32 -> F32,+depth: Nat,-values: Array<F32>,+position: U32,+context: Context,
  +witness: Witness.Witness(F32,depth,values)) -> Gathered<values,Lanes.gather(~Context,~map,values,position,context)>:
  +p1 = (position + 1 : U32)
  +p2 = (p1 + 1 : U32)
  +p3 = (p2 + 1 : U32)
  +p4 = (p3 + 1 : U32)
  +p5 = (p4 + 1 : U32)
  +p6 = (p5 + 1 : U32)
  +p7 = (p6 + 1 : U32)
  gathered(~Context,~map,values,position,context,Witness.read(F32,depth,values,position,witness),Witness.read(F32,depth,values,p1,witness),
    Witness.read(F32,depth,values,p2,witness),Witness.read(F32,depth,values,p3,witness),Witness.read(F32,depth,values,p4,witness),
    Witness.read(F32,depth,values,p5,witness),Witness.read(F32,depth,values,p6,witness),Witness.read(F32,depth,values,p7,witness))

Uses (10):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&name=Gathered
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&name=gathered
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather