def AP.of_list_eq

bend-osdev-array@0.1.0.1 · PROOF.bend:1347

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1347def AP.of_list_eq(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.of_list(T, d, xs, f) == AP.build(T, AP.tof(T, d, xs, f)) : Array<T>}:
1348  match d:
1349    case 0n:
1350      {==}
1351    case 1n+ +p:
1352      +s = A.Arrays.slots(p)
1353      +l = List.take(&2, T, xs, s)
1354      +r = List.drop(&2, T, xs, s)
1355      %Equal.sym(Array<T>, A.Arrays.of_list(T, p, l, f), AP.build(T, AP.tof(T, p, l, f)), AP.of_list_eq(T, p, l, f)) : {ANode{_, A.Arrays.of_list(T, p, r, f)} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
1356      %Equal.sym(Array<T>, A.Arrays.of_list(T, p, r, f), AP.build(T, AP.tof(T, p, r, f)), AP.of_list_eq(T, p, r, f)) : {ANode{AP.build(T, AP.tof(T, p, l, f)), _} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
1357      {==}