def AP.reflect

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

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

512def AP.reflect(-T: Data, a: Array<T>) -> &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}:
513  match a:
514    case ALeaf{x}:
515      (APLeaf{x}, {==})
516    case ANode{xs, ys}:
517      AP.reflect.join(T, xs, ys, AP.reflect(T, xs), AP.reflect(T, ys))

Uses (6)

Used by (10)