diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-08 23:03:21 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-08 23:03:21 +0100 |
| commit | ce3adde4b50ba04430a1cf0ffb0ea85168091746 (patch) | |
| tree | d2588c971eff856b117bb96b616eec1fab29c40a | |
| parent | d25444b11036504df09b60090a6fc86f99bd9ca7 (diff) | |
| download | vericert-kvx-ce3adde4b50ba04430a1cf0ffb0ea85168091746.tar.gz vericert-kvx-ce3adde4b50ba04430a1cf0ffb0ea85168091746.zip | |
End section in Abstr.v
| -rw-r--r-- | src/hls/Abstr.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 9bed783..957e265 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -736,6 +736,8 @@ Section CORRECT. Qed.*) Abort. +End CORRECT. + Lemma get_empty: forall r, empty#r = Psingle (Ebase r). Proof. |