pith. machine review for the scientific record. sign in
def definition def or abbrev

valueOfClause

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  38def valueOfClause {n} (σ : PartialAssignment n) (C : Clause n) : Option Bool :=

proof body

Definition body.

  39  let vals := C.map (valueOfLit σ)
  40  if vals.all Option.isSome then
  41    some (vals.any fun o => o.getD false)
  42  else
  43    none
  44
  45/-- Evaluate an XOR constraint under a partial assignment: returns `some b` if all
  46    vars are known, else none. -/

depends on (9)

Lean names referenced from this declaration's body.