From 9a65ca2731adf234f5ce946503314267ced62a44 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 23:19:48 +0100
Subject: Fix Inop proof to work with new array semantics.

---
 src/verilog/Array.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/verilog')

diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index 0b6e2a9..705dea7 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -83,6 +83,14 @@ Hint Resolve array_set_spec2 : array.
 Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
   nth_error a.(arr_contents) i.
 
+Lemma array_get_error_equal {A : Type} :
+  forall (a b : Array A) i,
+    a.(arr_contents) = b.(arr_contents) ->
+    array_get_error i a = array_get_error i b.
+Proof.
+  unfold array_get_error. congruence.
+Qed.
+
 Lemma array_get_error_bound {A : Type} :
   forall (a : Array A) i,
     i < a.(arr_length) -> exists x, array_get_error i a = Some x.
-- 
cgit