~/jendhub

def fresh

stelliferous@0.0.2.0 · proofs/storage_witness.bend:54

import stelliferous@0.0.2.0/proofs/storage_witness.bend as StorageWitness
import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape

54def fresh(-Element: Data,+depth: Nat,+value: Element) -> Witness(Element,depth,Array.new(Element,depth,value)):
55  %Equal.sym(Array<Element>,Array.new(Element,depth,value),Tree.pack(Element,Tree.fresh(Element,depth,value)),fresh_model(Element,depth,value)) : Witness(Element,depth,_)
56  from_shape(Element,depth,Tree.fresh(Element,depth,value),Shape.fresh(Element,depth,value))

Uses (10)

Used by (4)