def axis_complete
bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:120
import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
120def axis_complete(+left: U32, +right: U32, -output: Nat, +axis: Shape.Axis<U32.to_nat(left), U32.to_nat(right), output>) -> {Some{output} == choice_output(left, right, Shape.axis_choice(left, right)) : Maybe<&2, Nat>}:
121 axis_equal_complete(left, right, output, Shape.bool_case(Nat.is_eq(U32.to_nat(left), U32.to_nat(right))), axis)