PlanProofs.axis_left_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 94-105 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=94&end_line=105

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

def axis_left_complete(+left: U32, +right: U32, -output: Nat, +one: Shape.BoolCase<Nat.is_eq(1n, U32.to_nat(left))>, +axis: Shape.Axis<U32.to_nat(left), U32.to_nat(right), output>, differ: {False{} == Nat.is_eq(U32.to_nat(left), U32.to_nat(right)) : Bool}) -> {Some{output} == choice_output(left, right, Shape.axis_choice.left_one(left, right, one)) : Maybe<&2, Nat>}:
  match one:
    case Shape.BTrue{left_one}:
      match axis:
        case Shape.AxisEqual{left_eq, right_eq}:
          some_nat(output, U32.to_nat(right), right_eq)
        case Shape.AxisLeftOne{left_one_eq, right_eq}:
          some_nat(output, U32.to_nat(right), right_eq)
        case Shape.AxisRightOne{left_eq, right_one}:
          some_nat(output, U32.to_nat(right), Equal.trans(Nat, output, 1n, U32.to_nat(right), Equal.trans(Nat, output, U32.to_nat(left), 1n, left_eq, Equal.sym(Nat, 1n, U32.to_nat(left), Shape.equal_decided(1n, U32.to_nat(left), left_one))), right_one))
    case Shape.BFalse{left_wide}:
      axis_right_complete(left, right, output, Shape.bool_case(Nat.is_eq(1n, U32.to_nat(right))), axis, differ, left_wide)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.left_one
  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_right_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