PlanProofs.axis_complete: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
Lines 120-121 of bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&start_line=120&end_line=121

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

def 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>}:
  axis_equal_complete(left, right, output, Shape.bool_case(Nat.is_eq(U32.to_nat(left), U32.to_nat(right))), axis)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Axis
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=axis_choice
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=axis_equal_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=choice_output