def array_same

stelliferous@0.0.2.0 · proofs/storage_allocation_refinement.bend:46

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/storage_allocation.bend as Allocation

46def array_same(-Element: Data,+depth: Nat,+value: Element) ->
47  {Allocation.array(~Element,depth,value) == Array.new(Element,depth,value) : Array<Element>}:
48  %Equal.sym(Storage.Buffer<Element>,Allocation.allocate(~Element,depth,value,0n),Storage.allocate(~Element,depth,value,0n),
49    dispatch_same(Element,Allocation.allocated(~Element),depth,value,0n)) :
50    {Allocation.storage(~Element,_) == Array.new(Element,depth,value) : Array<Element>}
51  {==}