From 5d4aed9030565349a83f9ede4bd35c020eb416b5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 5 May 2020 00:38:19 +0100 Subject: Simplifications to proof --- src/verilog/Value.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'src/verilog/Value.v') diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 39d1832..61f2652 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -101,8 +101,6 @@ Definition boolToValue (sz : nat) (b : bool) : value := (** ** Arithmetic operations *) -Definition EQ_trivial : forall x, vsize x = vsize x. trivial. Defined. - Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. intros; subst; assumption. Defined. -- cgit