setVar
plain-language theorem explainer
The setVar definition supplies the pointwise update that overrides a single variable in a partial assignment while leaving all other entries unchanged. Authors formalizing SAT backpropagation or unit propagation would cite it when constructing the state transitions in BPStep. It is realized by a direct lambda that performs an equality test on the variable index.
Claim. Let $n$ be a natural number, let $σ$ map each index in $Fin n$ to an optional Boolean, let $v ∈ Fin n$, and let $b$ be a Boolean. Then setVar$(σ, v, b)$ is the function that returns some $b$ at index $v$ and returns $σ(w)$ at every other index $w$.
background
PartialAssignment $n$ is the type $Var n → Option Bool$, where $Var n$ is the abbreviation for $Fin n$. The module interprets none as an undetermined literal and some $b$ as a fixed Boolean value during backpropagation over CNF formulas that also carry an XORSystem. The local setting is therefore a state machine whose states are these partial maps, with transitions defined by guarded rules that refine the map.
proof idea
The definition is a one-line functional update expressed as a lambda that branches on whether the queried index equals the target variable.
why it matters
setVar is the primitive used inside the inductive clauses of BPStep and inside the proofs of bp_step_monotone, bp_step_sound, compatible_setVar, setVar_same and setVar_ne. These lemmas in turn establish that each propagation step preserves compatibility with any satisfying assignment of the underlying CNF and XOR constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.