StorageShape.store_node: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_shape.bend as StorageShape
Lines 41-51 of stelliferous@0.0.2.0/proofs/storage_shape.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&start_line=41&end_line=51

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

def store_node(-Element: Data,+depth: Nat,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,
  +half: U32,+index: U32,+value: Element,+choose_left: Bool,
  left_balanced: Balanced(Element,depth,left),right_balanced: Balanced(Element,depth,right),
  left_stored: Balanced(Element,depth,Tree.store(Element,left,half,index,value)),
  right_stored: Balanced(Element,depth,Tree.store(Element,right,half,(index - half : U32),value))) ->
  Balanced(Element,1n+depth,Bool.pick(Tree.Tree<Element>,choose_left,
    Tree.Node{Tree.store(Element,left,half,index,value),right},
    Tree.Node{left,Tree.store(Element,right,half,(index - half : U32),value)})):
  match choose_left:
    case True{}: Both{left_stored,right_balanced}
    case False{}: Both{left_balanced,right_stored}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  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=store