def axis_equal_complete

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:107

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

107def axis_equal_complete(+left: U32, +right: U32, -output: Nat, +same: Shape.BoolCase<Nat.is_eq(U32.to_nat(left), U32.to_nat(right))>, +axis: Shape.Axis<U32.to_nat(left), U32.to_nat(right), output>) -> {Some{output} == choice_output(left, right, Shape.axis_choice.equal(left, right, same)) : Maybe<&2, Nat>}:
108  match same:
109    case Shape.BTrue{equal}:
110      match axis:
111        case Shape.AxisEqual{left_eq, right_eq}:
112          some_nat(output, U32.to_nat(left), left_eq)
113        case Shape.AxisLeftOne{left_one, right_eq}:
114          some_nat(output, U32.to_nat(left), Equal.trans(Nat, output, U32.to_nat(right), U32.to_nat(left), right_eq, Equal.sym(Nat, U32.to_nat(left), U32.to_nat(right), Shape.equal_decided(U32.to_nat(left), U32.to_nat(right), equal))))
115        case Shape.AxisRightOne{left_eq, right_one}:
116          some_nat(output, U32.to_nat(left), left_eq)
117    case Shape.BFalse{differ}:
118      axis_left_complete(left, right, output, Shape.bool_case(Nat.is_eq(1n, U32.to_nat(left))), axis, differ)