Commit 784e2431 authored by Ralf Jung's avatar Ralf Jung

add timeless instance

parent 7810bc37
......@@ -28,6 +28,8 @@ Implicit Types vs : list val.
Implicit Types l : loc.
Implicit Types sz off : nat.
Global Instance array_timeless l vs : Timeless (array l vs) := _.
Lemma array_nil l : l ↦∗ [] ⊣⊢ emp.
Proof. by rewrite /array. Qed.
......
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