def AP.tof_perf

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

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

1359def AP.tof_perf(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.tof(T, d, xs, f))) == True{} : Bool}:
1360  match d:
1361    case 0n:
1362      {==}
1363    case 1n+ +p:
1364      +s = A.Arrays.slots(p)
1365      +l = List.take(&2, T, xs, s)
1366      +r = List.drop(&2, T, xs, s)
1367      %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.tof(T, p, l, f))), True{}, AP.tof_perf(T, p, l, f)) : {Bool.and(_, A.Arrays.is_perfect(T, p, AP.build(T, AP.tof(T, p, r, f)))) == True{} : Bool}
1368      AP.tof_perf(T, p, r, f)