AllocationPROOF.allocate_length: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationPROOF
Lines 16-23 of bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend&start_line=16&end_line=23

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation

def allocate_length(+depth: Nat, +length: Nat, +fill: F32, valid: Bool,
  -decision: {valid == Storage.bounds(depth, length) : Bool}, accepted: {valid == True{} : Bool}) ->
  {Allocation.storage_length(Storage.allocate(depth, length, fill, valid, decision)) == Some{length} : Maybe<&2, Nat>}:
  match valid:
    case False{}:
      Empty.absurd({None{} == Some{length} : Maybe<&2, Nat>}, Arith.clash(accepted))
    case True{}:
      {==}

Uses (9):
  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=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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/storage/main.bend&name=allocate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend&name=storage_length