Commit b831b8b5 authored by Mario Pereira's avatar Mario Pereira
Browse files

Schorr-Waite: updated sessions

parent 119e2920
......@@ -114,8 +114,7 @@ module SchorrWaite
requires { Seq.length stack > 0 }
ensures { result = stack[1 .. ] }
ensures { forall n. not_in_stack n stack -> not_in_stack n result }
=
stack[1 .. ]
= stack[1 .. ]
(** two lemmas about stacks *)
......
This diff is collapsed.
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