Theorem: BVExpr.eval_const (LeanSAT/Reflect/BVExpr/Basic.lean)

State before:
assign : Assignment
w✝ : Nat
val : BitVec w✝
⊢ eval assign (const val) = val
Tactic:
rfl
State after:
no goals