def written
stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:72
import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement
import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
72
73def written(+values: Tree.Tree<F32>,+position: U32,a: F32,b: F32,c: F32,d: F32,e: F32,f: F32,g: F32,h: F32) -> Tree.Tree<F32>:
74 +p1 = (position + 1 : U32)
75 +p2 = (p1 + 1 : U32)
76 +p3 = (p2 + 1 : U32)
77 +p4 = (p3 + 1 : U32)
78 +p5 = (p4 + 1 : U32)
79 +p6 = (p5 + 1 : U32)
80 +p7 = (p6 + 1 : U32)
81 Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,Tree.write(F32,values,position,a),p1,b),p2,c),p3,d),p4,e),p5,f),p6,g),p7,h)