def axis_right_complete

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:75

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

75def 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>}:
76  match one:
77    case Shape.BTrue{right_one}:
78      match axis:
79        case Shape.AxisEqual{left_eq, right_eq}:
80          some_nat(output, U32.to_nat(left), left_eq)
81        case Shape.AxisLeftOne{left_one, right_eq}:
82          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))
83        case Shape.AxisRightOne{left_eq, right_one_eq}:
84          some_nat(output, U32.to_nat(left), left_eq)
85    case Shape.BFalse{right_wide}:
86      match axis:
87        case Shape.AxisEqual{left_eq, right_eq}:
88          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))
89        case Shape.AxisLeftOne{left_one, right_eq}:
90          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))
91        case Shape.AxisRightOne{left_eq, right_one}:
92          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))