def store

stelliferous@0.0.2.0 · proofs/storage_tree_model.bend:40

import Base

40def store(-T: Data,tree: Tree<T>,+n: U32,+i: U32,+v: T) -> Tree<T>:
41  match tree:
42    case Leaf{old}:
43      Leaf{v}
44    case Node{+l,+r}:
45      Bool.pick(Tree<T>,U32.is_lt(i,U32.shr(n)),Node{store(T,l,U32.shr(n),i,v),r},Node{l,store(T,r,U32.shr(n),U32.sub(i,U32.shr(n)),v)})