def same_extent

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:595

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws

595def same_extent(+a: Nat, +b: Nat, +same: {a == b : Nat}, decision: Shape.BoolCase<Nat.is_eq(a, 1n)>) ->
596  {a == Laws.extent(a, b) : Nat}:
597  match decision:
598    case Shape.BTrue{equal}:
599      %equal : {a == Bool.pick(Nat, _, b, a) : Nat}
600      same
601    case Shape.BFalse{equal}:
602      %equal : {a == Bool.pick(Nat, _, b, a) : Nat}
603      {==}