diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-03 19:32:29 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-03 19:32:29 -0500 |
| commit | c342302d5dc80f254589dbe9ea0063b6ef34291f (patch) | |
| tree | 5d3acaf870c862787f7973da35c7b380c7f4cc97 /src/Util/FixedWordSizesEquality.v | |
| parent | 25132276ab23e6fd129802c5d90c09ddf72b3045 (diff) | |
Fix a typo
Diffstat (limited to 'src/Util/FixedWordSizesEquality.v')
| -rw-r--r-- | src/Util/FixedWordSizesEquality.v | 2 |
1 files changed, 1 insertions, 1 deletions
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)). |