lemma proved term proof

`parityOf_singleton`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  55@[simp] lemma parityOf_singleton {n} (a : Assignment n) (v : Var n) :
  56    parityOf a [v] = a v := by

Term-mode proof.

  57  simp [parityOf, List.foldl]
  58
  59/-- Helper: foldl with xor starting from init -/

Lean names referenced from this declaration's body.