def allocate_length

bendtorch-core@0.1.0.0 · src/tensor/allocation_PROOF.bend:16

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

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