def reflect

stelliferous@0.0.2.0 · proofs/storage_tree_model.bend:16

import Base

16# Proof observation of an existing owner, not a runtime conversion. Callers use
17# it only in erased propositions; numeric code continues to use Array directly.
18def reflect(-Element: Data,storage: Array<Element>) -> Tree<Element>:
19  match storage:
20    case ALeaf{value}: Leaf{value}
21    case ANode{left,right}: Node{reflect(Element,left),reflect(Element,right)}