skew heaps: small simplification

parent 1f741cb7
......@@ -5,7 +5,7 @@ module M
use import array.Array
type uf = { link : array int;
dist : array int; (* distance to representative *)
ghost dist : array int; (* distance to representative *)
num : int; (* number of classes *) }
function size (u: uf) : int = length u.link
......
......@@ -93,7 +93,7 @@ module SkewHeaps
let rec lemma root_is_min (t: tree elt) : unit
requires { heap t && 0 < size t }
ensures { is_minimum (minimum t) t }
variant { size t }
variant { t }
= match t with
| Empty -> absurd
| Node l _ r ->
......
......@@ -7,7 +7,7 @@
<file name="../skew_heaps.mlw" expanded="true">
<theory name="Heap" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SkewHeaps" sum="a25e10f51d8d90c6c5f0e6f4fc709a5b" expanded="true">
<theory name="SkewHeaps" sum="c18c50212e15bae26faeb36442258b60" expanded="true">
<goal name="WP_parameter root_is_min" expl="VC for root_is_min">
<transf name="split_goal_wp">
<goal name="WP_parameter root_is_min.1" expl="1. unreachable point">
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment