def ASet.top_get

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

import Base

2083def ASet.top_get(-T: Data, -a: Array<T>, +i: U32, +v: T, r: ASet.Copy(T, a)) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}:
2084  match r:
2085    case Tuple{b, r1}:
2086      match r1:
2087        case Tuple{+n, r2}:
2088          match r2:
2089            case Tuple{+p, r3}:
2090              match r3:
2091                case Tuple{+q, r4}:
2092                  %p : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), i)) == v : T}
2093                  ASet.close_get(T, b, n, i, v, q, ASet.facts(T, b, n, ASet.J(i, n), v, ASet.Z(i, n)))