ConstructionPROOF.construction_shape_complete: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
Lines 689-704 of bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&start_line=689&end_line=704

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend as Totality

def construction_shape_complete(+dimensions: List<&2, U32>, +values: List<&2, F32>, result: Shape.ConstructResult<dimensions>,
  built: {ShapeLaws.built(dimensions, result) == Some{dimensions} : Maybe<&2, List<&2, U32>>},
  +counted: {List.length(&2, F32, values) == Shape.logical_numel(dimensions) : Nat}) ->
  Totality.ConstructionDone<dimensions, Core.construct_shape(dimensions, values, result)>:
  match result:
    case Shape.SError{error}:
      Totality.ConstructionDone{
        Empty.absurd(Totality.ConstructionWitness<dimensions, Fail{Core.ShapeError{error}}>,
          Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Maybe.is_some(&2, List<&2, U32>), None{}, Some{dimensions}, built))),
        Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Maybe.is_some(&2, List<&2, U32>), None{}, Some{dimensions}, built), Unit{}}
    case Shape.SBuilt{+shape, +preserved}:
      construction_values_complete(dimensions, shape, preserved, Core.from_values(shape, values),
        from_values_complete(shape, values,
          %Equal.sym(List<&2, U32>, Shape.dimensions(shape), dimensions, preserved) :
            {List.length(&2, F32, values) == Shape.logical_numel(_) : Nat}
          counted))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=built
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=ConstructResult
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=construction_values_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=from_values_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend&name=ConstructionDone
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend&name=ConstructionWitness
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=construct_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=from_values