PlanProofs.axis_right_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 75-92 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=75&end_line=92

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

def axis_right_complete(+left: U32, +right: U32, -output: Nat, +one: Shape.BoolCase<Nat.is_eq(1n, U32.to_nat(right))>, +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}, left_wide: {False{} == Nat.is_eq(1n, U32.to_nat(left)) : Bool}) -> {Some{output} == choice_output(left, right, Shape.axis_choice.right_one(left, right, one)) : Maybe<&2, Nat>}:
  match one:
    case Shape.BTrue{right_one}:
      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}:
          Empty.absurd({Some{output} == Some{U32.to_nat(left)} : Maybe<&2, Nat>}, Nats.contradiction(Nat.is_eq(1n, U32.to_nat(left)), eq_true(1n, U32.to_nat(left), left_one), left_wide))
        case Shape.AxisRightOne{left_eq, right_one_eq}:
          some_nat(output, U32.to_nat(left), left_eq)
    case Shape.BFalse{right_wide}:
      match axis:
        case Shape.AxisEqual{left_eq, right_eq}:
          Empty.absurd({Some{output} == None{} : Maybe<&2, Nat>}, Nats.contradiction(Nat.is_eq(U32.to_nat(left), U32.to_nat(right)), eq_true(U32.to_nat(left), U32.to_nat(right), Equal.trans(Nat, U32.to_nat(left), output, U32.to_nat(right), Equal.sym(Nat, output, U32.to_nat(left), left_eq), right_eq)), differ))
        case Shape.AxisLeftOne{left_one, right_eq}:
          Empty.absurd({Some{output} == None{} : Maybe<&2, Nat>}, Nats.contradiction(Nat.is_eq(1n, U32.to_nat(left)), eq_true(1n, U32.to_nat(left), left_one), left_wide))
        case Shape.AxisRightOne{left_eq, right_one}:
          Empty.absurd({Some{output} == None{} : Maybe<&2, Nat>}, Nats.contradiction(Nat.is_eq(1n, U32.to_nat(right)), eq_true(1n, U32.to_nat(right), right_one), right_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=Empty.absurd
  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.right_one
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=contradiction
  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=eq_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=some_nat