mk: phase 5D — matche pattern matching, phase 5 complete

Pattern grammar: _, symbol, atom (number/string/keyword/bool), (), and
(p1 ... pn) list patterns (recursive). Symbols become fresh vars in a
fresh form, atoms become literals to unify against, lists recurse
position-wise. Repeated names produce the same fresh var (so they
unify by ==).

Macro is built with explicit cons/list rather than a quasiquote because
the quasiquote expander does not recurse into nested lambda bodies —
the natural `\`(matche-clause (quote ,target) cl)` spelling left
literal `(unquote target)` forms in the output.

14 tests, 222/222 cumulative. Phase 5 done (project, conda, condu,
onceo, nafc, matche all green).

plans/minikanren-on-sx.md

@@ -125,8 +125,13 @@ Key semantic mappings:
 - [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)`
       in the body's lexical scope, then runs `(mk-conj body...)` on the same
       substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
-- [ ] `matche` — pattern matching over logic terms (extension from core.logic)
-      `(matche l ((head . tail) goal) (() goal))`
+- [x] `matche` — pattern matching over logic terms. Pattern grammar: `_` /
+      symbol / atom / `()` / `(p1 p2 ... pn)`. Each clause becomes
+      `(fresh (vars-in-pat) (== target pat-expr) body...)`. Repeated symbol
+      names in a pattern produce the same fresh var, so they unify (== check).
+      Built without quasiquote (the expander does not recurse into lambda
+      bodies). Fixed-length list patterns only — head/tail destructuring uses
+      `(fresh (a d) (conso a d target) body)` directly.
 - [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
       flow through rest-goals; later clauses not tried (`Phase 5 piece A`)
 - [x] `condu` — committed choice (Phase 2)
@@ -161,6 +166,13 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-08** — **Phase 5 piece D — matche, Phase 5 done**: pattern matching
+  macro (`lib/minikanren/matche.sx`) — symbols become fresh vars, atoms become
+  literals, lists recurse positionally, repeated names unify. 14 new tests
+  (literals, vars, wildcards, list patterns, multi-clause dispatch, nested
+  patterns, repeated-var-implies-eq). Built via `cons`/`list` rather than
+  quasiquote because SX's quasiquote does not recurse into lambda bodies — a
+  worth-knowing gotcha. 222/222 cumulative.
 - **2026-05-08** — **Phase 4 piece C — permuteo + inserto**: standard recursive
   insert-at-any-position + permute-tail. 7 new tests, including all-6-perms-of-3
   as a set check. 208/208 cumulative.