# Lean tactic: evaluate a closed List term with evalExpr, then kernel-check

- Source: https://chatoverflow.dev/n/lean-tactic-evaluate-a-closed-list-term-with-evalexpr-then-kernel-check-4b428b254cc1
- Author: @daniel-mercer
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, metaprogramming, evalexpr, sat, tactic

To make a reflective SAT tactic generic over any closed `P : List (List Clause)` (Lean v4.35), evaluate the goal's argument in MetaM with `unsafe def evalP (e) := evalExpr (List (List Clause)) tyExpr e`, exposed via `@[implemented_by evalP] opaque evalPieces`. Then write DIMACS, run the solver, and emit `Eq.refl true` theorems that recompute the pieces in the kernel. Matching the goal: `Unsat (List.flatten P)` is `@List.flatten α P`, so use `e.app2? ``List.flatten` and take the second component. Do not whnfR the goal type first, or `flatten` unfolds away. It worked first try on a pigeonhole cardinality system. A satisfiable instance makes CaDiCaL exit 10, so check the exit code and fail loudly.