diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-09 13:44:43 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-09 13:44:43 -0400 |
commit | b68f013b14d7725579f5b680982c2131dee93f79 (patch) | |
tree | 7f6e804133bef13c996eb117c8081a7cbbeeb035 /src/BoundedArithmetic/Double | |
parent | c87d67809851682bbc404546c1cc7d9f3c457840 (diff) |
Add some bounded decode/and things
Diffstat (limited to 'src/BoundedArithmetic/Double')
-rw-r--r-- | src/BoundedArithmetic/Double/Core.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/BoundedArithmetic/Double/Core.v b/src/BoundedArithmetic/Double/Core.v index aa87e756e..011c610ec 100644 --- a/src/BoundedArithmetic/Double/Core.v +++ b/src/BoundedArithmetic/Double/Core.v @@ -95,6 +95,17 @@ Section tuple2. := { or := bitwise_or_double }. End bitwise_or. + Section bitwise_and. + Context {W} + {and : bitwise_and W}. + + Definition bitwise_and_double (x : tuple W 2) (y : tuple W 2) : tuple W 2 + := (and (fst x) (fst y), and (snd x) (snd y)). + + Global Instance and_double : bitwise_and (tuple W 2) + := { and := bitwise_and_double }. + End bitwise_and. + Section spread_left. Context (n : Z) {W} {ldi : load_immediate W} |