def allowed_true

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:266

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

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