def matched_chosen

bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:137

import Base
import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold
import bendtorch-core@0.1.0.0/src/tensor/contracts/sum.bend as Sum
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

137def matched_chosen(+same: Bool, +total: F32, +word: F32) ->
138  {ReduceLaws.matched(Some{total}, Some{word}, same) == Some{Fold.chosen(~Unit, ~Sum.add, Unit{}, same, total, word)} : Maybe<&2, F32>}:
139  match same:
140    case False{}:
141      {==}
142    case True{}:
143      {==}