Commit bc6dbed9 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

initial testing

parent f410e4e7
Pipeline #19385 failed with stage
in 0 seconds
......@@ -138,5 +138,6 @@ Lemma rotate_l_spec x y z v1 v2 v3 :
{{{ RET #(); x v2 y v3 z v1 }}}.
Proof.
(* exercise *)
Admitted.
End proof.
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