StorageTreeModel.reflect: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as StorageTreeModel
Lines 16-21 of stelliferous@0.0.2.0/proofs/storage_tree_model.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&start_line=16&end_line=21

import Base

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

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree