Commit 298a38f3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix typo.

parent a5672181
...@@ -43,7 +43,7 @@ module TreeOfList ...@@ -43,7 +43,7 @@ module TreeOfList
let tree_of_list (l: list elt) : tree elt let tree_of_list (l: list elt) : tree elt
ensures { inorder result = l } ensures { inorder result = l }
ensures { size result > 0 -> let h = height result in ensures { size result > 0 -> let h = height result in
- power 2 (h-1) <= size result < power 2 h } power 2 (h-1) <= size result < power 2 h }
= =
let t, l = tree_of_list_aux (length l) l in let t, l = tree_of_list_aux (length l) l in
assert { l = Nil }; assert { l = Nil };
......
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