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

Clause

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)

  41structure Clause (n : ℕ) where
  42  /-- Up to 3 literal indices in {1,..,n} with signs -/
  43  literals : List (Fin n × Bool)
  44  /-- At most 3 literals per clause -/
  45  size_bound : literals.length ≤ 3
  46
  47/-- A k-CNF formula is a list of clauses over n variables. -/

used by (16)

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

depends on (30)

Lean names referenced from this declaration's body.