def read_fresh

stelliferous@0.0.2.0 · proofs/storage_readback.bend:165

import stelliferous@0.0.2.0/proofs/storage_readback.bend as StorageReadback

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

165def read_fresh(~Element: Data,+depth: Nat,+value: Element,+index: U32) -> {Tree.read(Element,Tree.fresh(Element,depth,value),index) == value : Element}:
166  fetch_fresh(~Element,depth,value,Tree.capacity(Element,Tree.fresh(Element,depth,value)),U32.and(index,U32.sub(Tree.capacity(Element,Tree.fresh(Element,depth,value)),1)))

Uses (8)

U32
Nat
U32.sub
U32.and
stelliferous@0.0.2.0/proofs/storage_tree_model:capacity
…

Used by (0)

No other definition uses this definition.