PlanProofs.axis_equal_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 107-118 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=107&end_line=118

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

def 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>}:
  match same:
    case Shape.BTrue{equal}:
      match axis:
        case Shape.AxisEqual{left_eq, right_eq}:
          some_nat(output, U32.to_nat(left), left_eq)
        case Shape.AxisLeftOne{left_one, right_eq}:
          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))))
        case Shape.AxisRightOne{left_eq, right_one}:
          some_nat(output, U32.to_nat(left), left_eq)
    case Shape.BFalse{differ}:
      axis_left_complete(left, right, output, Shape.bool_case(Nat.is_eq(1n, U32.to_nat(left))), axis, differ)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=axis_choice.equal
  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/core.bend&name=equal_decided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=axis_left_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=choice_output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=some_nat