```  #line 13 "/home/travis/build/felix-lang/felix/src/packages/trees.fdoc"
class MinHeap[T with Tord[T]]
{
fun left_child (p:int)  => 2*p + 1;
fun right_child (p:int) => 2*p + 2;
fun parent (c:int) => if c == 0 then 0 else (c - 1)/2;

axiom family (i:int): i == i.left_child.parent and i == i.right_child.parent;
typedef minheap_t = darray[T];
ctor minheap_t () => darray[T] ();
axiom left_heap (m:minheap_t, i:int):
i.left_child < m.len.int or m.i < m.(i.left_child)
;

proc heap_swap (h:minheap_t,i:int,j:int) {
var tmp = h.i;
set(h,i,h.j);
set(h,j,tmp);
}

proc bubble_up(h:minheap_t, j:int)
{
var p = parent j; // parent of root is itself
if h.p > h.j do // and so can't satisfy this condition
heap_swap(h,p,j);
bubble_up(h,p);
done
}
proc heap_insert (h:minheap_t) (elt:T) {
push_back (h,elt);
bubble_up (h,h.len.int - 1);
}

// this procedure does nothing if the index p
// is greater than or equal to the limit - 2,
// since the last used slot is lim - 1,
// and that node cannot have any children.
proc bubble_down_lim (h:minheap_t, p:int, lim:int) {
var min_index = p;
var left = p.left_child;
if left < lim do
if h.min_index > h.left perform min_index = left;
var right = left + 1;
if right < lim
if h.min_index > h.right perform min_index = right;
done
if min_index != p do
heap_swap (h, p, min_index);
bubble_down_lim (h, min_index, lim);
done
}

proc bubble_down (h:minheap_t,p:int) =>
bubble_down_lim (h, p, h.len.int)
;

gen extract_min (h:minheap_t) : opt[T] =  {
if h.len.int == 0 return None[T];
var min = h.0;
set(h,0,h.(h.len.int - 1));
h.pop;
bubble_down (h,0);
return Some min;
}

// sorts largest to smallest!!
// based on extract_min, except the minimum element
// is moved to the position at the end of the heap
// which would otherwise be deleted.
proc heap_sort (h:minheap_t) {
var tosort = h.len.int;
while tosort > 1 do
--tosort;
heap_swap(h,0,tosort);
bubble_down_lim (h,0, tosort);
done
}

proc heapify (h:minheap_t) {
var index = h.len.int - 2;
while index >= 0 do
bubble_down (h, index); --index;
done
}

}
```