TraversalLanesCertificate.gather: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend as TraversalLanesCertificate
Lines 71-79 of stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend&start_line=71&end_line=79

import Base
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as LanesWitness

def gather(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,+position: U32,+context: Context,
  certificate: Certificate.Certificate<F32,values>) ->
  Certificate.Certificate<F32,TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context))>:
  Certificate.Certificate{+depth,+equation} = certificate
  %Equal.sym(Array<F32>,TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)),values,
    gathered_owner(~Context,~map,values,position,context,
      LanesWitness.gather(~Context,~map,depth,values,position,context,Certificate.witness_at(F32,depth,values,equation)))) :
    Certificate.Certificate<F32,_>
  Certificate.Certificate{depth,equation}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=witness_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend&name=gathered_owner
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=gather