def ASet.top_size

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

import Base

2071def ASet.top_size(-T: Data, -a: Array<T>, +i: U32, +v: T, r: ASet.Copy(T, a)) -> {ASet.sz(T, Array.set(T, a, i, v)) == ASet.sz(T, a) : U32}:
2072  match r:
2073    case Tuple{b, r1}:
2074      match r1:
2075        case Tuple{+n, r2}:
2076          match r2:
2077            case Tuple{+p, r3}:
2078              match r3:
2079                case Tuple{+q, r4}:
2080                  %p : {ASet.sz(T, Array.set(T, _, i, v)) == ASet.sz(T, _) : U32}
2081                  ASet.close_size(T, b, n, i, v, q, ASet.facts(T, b, n, ASet.J(i, n), v, ASet.Z(i, n)))