From 4884a324ed0fa3a8602777bdb49580e801ff6f5b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 3 Oct 2020 20:06:11 +0100 Subject: Add proof of splitlong_ptr32 --- verilog/Archi.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/verilog/Archi.v b/verilog/Archi.v index e59274e2..8f1ccdef 100644 --- a/verilog/Archi.v +++ b/verilog/Archi.v @@ -28,6 +28,9 @@ Definition align_float64 := 4%Z. Definition splitlong := false. +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. discriminate. Qed. + Definition default_nan_64 := (true, iter_nat 51 _ xO xH). Definition default_nan_32 := (true, iter_nat 22 _ xO xH). -- cgit