From 3ab94bace08b3c9b74bb6d137485611e45e28a68 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 21 Apr 2021 12:32:03 +0200
Subject: [PATCH] comment

---
 theories/bitvector.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/bitvector.v b/theories/bitvector.v
index a8255a4a..798d2111 100644
--- a/theories/bitvector.v
+++ b/theories/bitvector.v
@@ -517,7 +517,9 @@ Program Definition bv_sign_extend {n} (z : N) (b : bv n) : bv (n + z) := (* SMT:
 
 (* s is start index and l is length. Note that this is different from
 extract in SMTLIB which uses [extract (inclusive upper bound)
-(inclusive lower bound)] *)
+(inclusive lower bound)]. The version here is phrased in a way that
+makes it impossible to use an upper bound that is lower than the lower
+bound. *)
 Program Definition bv_extract {n} (s l : N) (b : bv n) : bv l :=
   BV l (Z.land (bv_unsigned b ≫ Z.of_N s) (Z.ones (Z.of_N l))) _.
 Next Obligation.
-- 
GitLab