TensorLayout.surveyed: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_layout.bend as TensorLayout
Lines 285-292 of stelliferous@0.0.2.0/tensor_layout.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/tensor_layout.bend&start_line=285&end_line=292

import Base
import stelliferous@0.0.2.0/tensor_shape.bend as Shapes
import stelliferous@0.0.2.0/tensor.bend as Tensors

def surveyed(survey: Survey,+first: List<&2,U32>,+shape: List<&2,U32>,+axis: Nat,status: Tensors.Status,workers: U32) -> Survey:
  Survey{valid,+total,previous,most} = survey
  +width = extent_at(shape,axis)
  Survey{valid && Nat.is_eq(List.length(&2,U32,first),List.length(&2,U32,shape)) &&
      Shapes.same_extents(List.take(&2,U32,first,axis),List.take(&2,U32,shape,axis)) &&
      Shapes.same_extents(List.drop(&2,U32,first,1n+axis),List.drop(&2,U32,shape,1n+axis)) &&
      U32.is_le(width,(4294967295 - total : U32)),
    (total + width : U32),Tensors.first_failure(previous,status),U32.max(most,workers)}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  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=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.max
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor.bend&name=Status
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor.bend&name=first_failure
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_layout.bend&name=Survey
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_layout.bend&name=extent_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_shape.bend&name=same_extents