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 /src | |
parent | d25444b11036504df09b60090a6fc86f99bd9ca7 (diff) | |
download | vericert-ce3adde4b50ba04430a1cf0ffb0ea85168091746.tar.gz vericert-ce3adde4b50ba04430a1cf0ffb0ea85168091746.zip |
End section in Abstr.v
Diffstat (limited to 'src')
-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. |