module heap
type multiway-treeck/heap/multiway-tree: V -> V<aa: V>
Empck/heap/Emp: forall<a> multiway-tree<a>
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>{ valuevalue: 5: aa: V; subsub: list<multiway-tree<5>>: liststd/core/list: V -> V<multiway-treeck/heap/multiway-tree: V -> V<aa: V>> }
}
pub inline fun is-emptyck/heap/is-empty: forall<a> (h : pairing-heap<a>) -> bool(hh: pairing-heap<$165>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): boolstd/core/types/bool: V
match hh: pairing-heap<$165>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>
Empck/heap/Emp: forall<a> multiway-tree<a> -> Truestd/core/types/True: bool
_ -> Falsestd/core/types/False: bool
pub inline fun emptyck/heap/empty: forall<a> (comp : (a, a) -> order) -> pairing-heap<a>(compcomp: ($152, $152) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(Empck/heap/Emp: forall<a> multiway-tree<a>, compcomp: ($152, $152) -> order)
pub inline fun singletonck/heap/singleton: forall<a> (v : a, comp : (a, a) -> order) -> pairing-heap<a>(vv: $203: aa: V, compcomp: ($203, $203) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $203, [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>), compcomp: ($203, $203) -> order)
fun meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(t1t1: multiway-tree<$222>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, t2t2: multiway-tree<$222>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, compcomp: ($222, $222) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): multiway-treeck/heap/multiway-tree: V -> V<aa: V>
match t1t1: multiway-tree<$222>
Empck/heap/Emp: forall<a> multiway-tree<a> -> t2t2: multiway-tree<$222>
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v1v1: $222, ss1ss1: list<multiway-tree<$222>>) ->
match t2t2: multiway-tree<$222>
Empck/heap/Emp: forall<a> multiway-tree<a> -> t1t1: multiway-tree<$222>
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v2v2: $222, ss2ss2: list<multiway-tree<$222>>) ->
if compcomp: ($222, $222) -> order(v1v1: $222, v2v2: $222).is-ltstd/core/types/is-lt: (order : order) -> bool then
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v1v1: $222, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t2t2: multiway-tree<$222>, ss1ss1: list<multiway-tree<$222>>))
else
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(v2v2: $222, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t1t1: multiway-tree<$222>, ss2ss2: list<multiway-tree<$222>>))
pub inline fun meldck/heap/meld.1: forall<a> (h1 : pairing-heap<a>, h2 : pairing-heap<a>) -> pairing-heap<a>(h1h1: pairing-heap<$271>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, h2h2: pairing-heap<$271>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(h1h1: pairing-heap<$271>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>, h2h2: pairing-heap<$271>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>, h1h1: pairing-heap<$271>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order)), h1h1: pairing-heap<$271>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order))
fun insertck/heap/insert: forall<a> (t : multiway-tree<a>, v : a, comp : (a, a) -> order) -> multiway-tree<a>(tt: multiway-tree<$420>: multiway-treeck/heap/multiway-tree: V -> V<aa: V>, vv: $420: aa: V, compcomp: ($420, $420) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): multiway-treeck/heap/multiway-tree: V -> V<aa: V>
match tt: multiway-tree<$420>
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(aa: $420, ssss: list<multiway-tree<$420>>) ->
if compcomp: ($420, $420) -> order(vv: $420, aa: $420).is-ltstd/core/types/is-lt: (order : order) -> bool then
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $420, [std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>tt: multiway-tree<$420>]std/core/Nil: forall<a> list<a>)
else
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(aa: $420, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $420, [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>), ssss: list<multiway-tree<$420>>))
Empck/heap/Emp: forall<a> multiway-tree<a> -> Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $420, [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>)
pub inline fun insertck/heap/insert.1: forall<a> (h : pairing-heap<a>, v : a) -> pairing-heap<a>(hh: pairing-heap<$472>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>, vv: $472: aa: V): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(hh: pairing-heap<$472>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>.insertck/heap/insert: forall<a> (t : multiway-tree<a>, v : a, comp : (a, a) -> order) -> multiway-tree<a>(vv: $472, hh: pairing-heap<$472>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order)), hh: pairing-heap<$472>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order))
pub inline fun minck/heap/min: forall<a> (h : pairing-heap<a>) -> maybe<a>(hh: pairing-heap<$181>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): maybestd/core/types/maybe: V -> V<aa: V>
match hh: pairing-heap<$181>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>
Empck/heap/Emp: forall<a> multiway-tree<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(vv: $181, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(vv: $181)
fun meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, comp : (a, a) -> order) -> multiway-tree<a>(tsts: list<multiway-tree<$326>>: liststd/core/list: V -> V<multiway-treeck/heap/multiway-tree: V -> V<aa: V>>, compcomp: ($326, $326) -> order: (aa: V, aa: V) -> orderstd/core/types/order: V): multiway-treeck/heap/multiway-tree: V -> V<aa: V>
match tsts: list<multiway-tree<$326>>
Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t1t1: multiway-tree<$326>, Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(t2t2: multiway-tree<$326>, ts'ts': list<multiway-tree<$326>>)) -> meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(meldck/heap/meld: forall<a> (t1 : multiway-tree<a>, t2 : multiway-tree<a>, comp : (a, a) -> order) -> multiway-tree<a>(t1t1: multiway-tree<$326>, t2t2: multiway-tree<$326>, compcomp: ($326, $326) -> order), ts'ts': list<multiway-tree<$326>>.meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, comp : (a, a) -> order) -> multiway-tree<a>(compcomp: ($326, $326) -> order), compcomp: ($326, $326) -> order)
[std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a> -> Empck/heap/Emp: forall<a> multiway-tree<a>
[tstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>]std/core/Nil: forall<a> list<a> -> tt: multiway-tree<$326>
pub inline fun erase-minck/heap/erase-min: forall<a> (h : pairing-heap<a>) -> pairing-heap<a>(hh: pairing-heap<$384>: pairing-heapck/heap/pairing-heap: V -> V<aa: V>): pairing-heapck/heap/pairing-heap: V -> V<aa: V>
match hh: pairing-heap<$384>.treeck/heap/tree: forall<a> (pairing-heap<a>) -> multiway-tree<a>
Empck/heap/Emp: forall<a> multiway-tree<a> -> hh: pairing-heap<$384>
Brack/heap/Bra: forall<a> (value : a, sub : list<multiway-tree<a>>) -> multiway-tree<a>(_, ssss: list<multiway-tree<$384>>) -> Heapck/heap/Heap: forall<a> (tree : multiway-tree<a>, comp : (a, a) -> order) -> pairing-heap<a>(ssss: list<multiway-tree<$384>>.meld-pairsck/heap/meld-pairs: forall<a> (ts : list<multiway-tree<a>>, comp : (a, a) -> order) -> multiway-tree<a>(hh: pairing-heap<$384>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order)), hh: pairing-heap<$384>.compck/heap/comp: forall<a> (pairing-heap<a>) -> ((a, a) -> order))