StorageWitness.from_shape: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_witness.bend as StorageWitness
Lines 35-43 of stelliferous@0.0.2.0/proofs/storage_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&start_line=35&end_line=43

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape

def from_shape(-Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,balanced: Shape.Balanced(Element,depth,tree)) ->
  Witness(Element,depth,Tree.pack(Element,tree)):
  match depth tree:
    case 0n Tree.Leaf{value}: Leaf{value,{==}}
    case 0n Tree.Node{left,right}: match balanced:
    case 1n+rest Tree.Leaf{value}: match balanced:
    case 1n+ +rest Tree.Node{+left,+right}:
      Shape.Both{left_balanced,right_balanced} = balanced
      Node{Tree.pack(Element,left),Tree.pack(Element,right),{==},from_shape(Element,rest,left,left_balanced),from_shape(Element,rest,right,right_balanced)}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=LeafWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=NodeWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness