def ASet.close_size

bend-ml-tensor-array@0.1.19.0 · main.bend:2041

import Base

2041def ASet.close_size(-T: Data, -b: Array<T>, +n: U32, +i: U32, +v: T, +q: {n == ASet.sz(T, b) : U32}, f: ASet.Facts(T, b, n, ASet.J(i, n), v, ASet.Z(i, n))) -> {ASet.sz(T, Array.set(T, b, i, v)) == ASet.sz(T, b) : U32}:
2042  match f:
2043    case Tuple{+c1, r1}:
2044      match r1:
2045        case Tuple{+c2, r2}:
2046          match r2:
2047            case Tuple{+c3, r3}:
2048              match r3:
2049                case Tuple{+c4, r4}:
2050                  %c1 : {ASet.sz(T, Array.set.fin(T, Array.swap.at(T, i, v, _))) == ASet.sz(T, b) : U32}
2051                  %q : {ASet.sz(T, Array.set.fin(T, Array.swap.go(T, b, _, ASet.J(i, _), v, ASet.Z(i, _)))) == _ : U32}
2052                  Equal.trans(U32, ASet.sz(T, ASet.NA(T, b, n, ASet.J(i, n), v, ASet.Z(i, n))), ASet.sz(T, b), n, c4, Equal.sym(U32, n, ASet.sz(T, b), q))