From c342302d5dc80f254589dbe9ea0063b6ef34291f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 3 Feb 2017 19:32:29 -0500 Subject: Fix a typo --- src/Util/FixedWordSizesEquality.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/FixedWordSizesEquality.v') diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 620b79f67..9ae21d548 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -187,7 +187,7 @@ Local Ltac wordToZ_word_case_dep_t := change 32%nat with (2^5)%nat in *; apply H. -Lemma wordToZ_word_case_dep_1op (wop : forall sz, word sz -> word sz) +Lemma wordToZ_word_case_dep_unop (wop : forall sz, word sz -> word sz) (P : nat -> Z -> Z -> Type) : (forall logsz (x : word (2^logsz)), P logsz (wordToZ_gen x) (wordToZ_gen (wop (2^logsz) x))) -> forall logsz (x : wordT logsz), P logsz (wordToZ x) (wordToZ (word_case_dep (T:=fun _ W => W -> W) logsz (wop 32) (wop 64) (wop 128) (fun _ => wop _) x)). -- cgit v1.2.3