Skip to content
Snippets Groups Projects
Commit 1cf6659d authored by Michael Sammler's avatar Michael Sammler
Browse files

fix typo

parent 809dee91
No related branches found
No related tags found
No related merge requests found
Pipeline #70639 passed
...@@ -9,7 +9,7 @@ From stdpp Require Import options. ...@@ -9,7 +9,7 @@ From stdpp Require Import options.
(** * [bitblast] tactic: Solve integer goals by bitwise reasoning *) (** * [bitblast] tactic: Solve integer goals by bitwise reasoning *)
(** This file provides the [bitblast] tactic for bitwise reasoning (** This file provides the [bitblast] tactic for bitwise reasoning
about [Z] via [Z.testbit]. Concretely, [bitblast] first turns an 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 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.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)] [Z.testbit (Z.ones z) n = bool_decide (0 ≤ n < z) || bool_decide (z < 0 ∧ 0 ≤ n)]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment