def other_operand

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:147

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

147def other_operand(x: Bool, y: Bool, both: {Bool.and(x, Bool.not(y)) == True{} : Bool}) -> {y == False{} : Bool}:
148  match x:
149    case False{}:
150      Empty.absurd({y == False{} : Bool}, Arith.clash(both))
151    case True{}:
152      match y:
153        case True{}:
154          Empty.absurd({True{} == False{} : Bool}, Arith.clash(both))
155        case False{}:
156          {==}