def maybe_equal

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:108

import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
import Base
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle

108def maybe_equal(+a: Maybe<&2, List<&2, U32>>, +b: Maybe<&2, List<&2, U32>>,
109  equal: {True{} == Layout.maybe_same(a, b) : Bool}) -> {a == b : Maybe<&2, List<&2, U32>>}:
110  match a b:
111    case None{} None{}:
112      {==}
113    case Some{xs} Some{ys}:
114      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, xs => Some{xs}, xs, ys, words_equal(xs, ys, equal))
115    case None{} Some{ys}:
116      Empty.absurd({None{} == Some{ys} : Maybe<&2, List<&2, U32>>}, Lifecycle.false_true(equal))
117    case Some{xs} None{}:
118      Empty.absurd({Some{xs} == None{} : Maybe<&2, List<&2, U32>>}, Lifecycle.false_true(equal))

Uses (9)

Used by (1)