This module contains the verification of the bitblaster for BitVec.reverse
from
Impl.Operations.Reverse
.
@[simp]
theorem
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastReverse
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Sat.AIG α)
(target : aig.RefVec w)
(assign : α → Bool)
(idx : Nat)
(hidx : idx < w)
: