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

clauseUnit

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)

  66def clauseUnit {n} (σ : PartialAssignment n) (C : Clause n) : Option (Var n × Bool) :=

proof body

Definition body.

  67  let vals := C.map (valueOfLit σ)
  68  let unknowns := C.zip vals |>.filter (fun ⟨_, o⟩ => o.isNone)
  69  if h1 : unknowns.length = 1 then
  70    if (vals.filter Option.isSome).all (fun o => o.getD false = false) then
  71      let l := unknowns.get ⟨0, by omega⟩
  72      match l.fst with
  73      | .pos v => some (v, true)
  74      | .neg v => some (v, false)
  75    else none
  76  else none
  77
  78/-- A (single) backpropagation step relation with guarded rules. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.