def axis_left_complete

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

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

94def 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>}:
95  match one:
96    case Shape.BTrue{left_one}:
97      match axis:
98        case Shape.AxisEqual{left_eq, right_eq}:
99          some_nat(output, U32.to_nat(right), right_eq)
100        case Shape.AxisLeftOne{left_one_eq, right_eq}:
101          some_nat(output, U32.to_nat(right), right_eq)
102        case Shape.AxisRightOne{left_eq, right_one}:
103          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))
104    case Shape.BFalse{left_wide}:
105      axis_right_complete(left, right, output, Shape.bool_case(Nat.is_eq(1n, U32.to_nat(right))), axis, differ, left_wide)