143def encodeClause (g : ClauseGadget n) (assignment : Fin n → Bool) : Window g.width :=
proof body
Definition body.
144 fun i => 145 if i.val < g.variables.length then 146 let var_idx := g.variables.get! i.val 147 let neg := g.negated.get! i.val 148 let val := assignment var_idx 149 if neg then (if val then .Zero else .One) 150 else (if val then .One else .Zero) 151 else if i.val = g.variables.length then 152 .Gate -- OR gate 153 else 154 .Wire 155 156/-- A full SAT instance encoded as CA tape -/
depends on (15)
Lean names referenced from this declaration's body.