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# Eight ordered writes from position.
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)

Uses (5)

Used by (1)