ReductionPROOF.allowed_true: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 266-273 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=266&end_line=273

import Base
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle

def allowed_true(+depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, allowed: Bool, +value: F32,
  observed: {Lifecycle.observe_allowed(depth, length, array, index, allowed) == Some{value} : Maybe<&2, F32>}) ->
  {allowed == True{} : Bool}:
  match allowed:
    case False{}:
      Empty.absurd({False{} == True{} : Bool}, no_value(value, observed))
    case True{}:
      {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=observe_allowed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=no_value