aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Core.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-26 00:34:03 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-06-26 10:02:10 -0400
commit689bd71a2a5afd5ce652ff123252f163f5047b74 (patch)
treeb0743697e6daacd38ff9e45274910d880306b04d /src/Arithmetic/Core.v
parentb259663f37d8cf05ad247c1fe3232b08f6e09e8b (diff)
Add nonzero synthesis
Diffstat (limited to 'src/Arithmetic/Core.v')
-rw-r--r--src/Arithmetic/Core.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 5794659da..457a85a98 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -307,6 +307,8 @@ Definition runtime_and := Z.land.
Global Notation "a &' b" := (runtime_and a%RT b%RT) : runtime_scope.
Definition runtime_shr := Z.shiftr.
Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope.
+Definition runtime_lor := Z.lor.
+Global Arguments runtime_lor (_ _)%RT.
Module B.
Definition limb := (Z*Z)%type. (* position coefficient and run-time value *)