StorageAllocationRefinement.array_same: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend as StorageAllocationRefinement
Lines 46-51 of stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend&start_line=46&end_line=51

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

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

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend&name=dispatch_same
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=allocate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=allocated
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=array
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=storage
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_buffer.bend&name=Buffer
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_buffer.bend&name=allocate