diff --git a/stdpp_unstable/bitblast.v b/stdpp_unstable/bitblast.v index d8f71e5ac5943467cfdc8d58d23ce0bd1c973c43..04931c2849f1f61f56f389bd9dd6bf9de9aaa197 100644 --- a/stdpp_unstable/bitblast.v +++ b/stdpp_unstable/bitblast.v @@ -9,7 +9,7 @@ From stdpp Require Import options. (** * [bitblast] tactic: Solve integer goals by bitwise reasoning *) (** This file provides the [bitblast] tactic for bitwise reasoning about [Z] via [Z.testbit]. Concretely, [bitblast] first turns an -equality [a = b] into [∀ n, Z.testbit a n = Z.testbit a b], then +equality [a = b] into [∀ n, Z.testbit a n = Z.testbit b n], then simplifies the [Z.testbit] expressions using lemmas like [Z.testbit (Z.land a b) n = Z.testbit a n && Z.testbit b n], or [Z.testbit (Z.ones z) n = bool_decide (0 ≤ n < z) || bool_decide (z < 0 ∧ 0 ≤ n)]