diff --git a/lib/check.ml b/lib/check.ml
index 12b6219..bad8782 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1054,6 +1054,59 @@ and named_call ctx ~want loc name args =
          "zeroed needs to know the type it is zeroing — use it where one is \
           expected, as in (set grid (zeroed))")
 
+  (* The one half of a destructuring [let] that [Parse] cannot do on its own.
+     Everything else about a pattern is bindings and field accesses it already
+     wrote; the arity is a *type* question — how many elements the value has —
+     and there are no types in the parser. So the pattern's shape travels here
+     as arguments: which element this binding wants, how many names the pattern
+     binds, and whether that count is exact or a minimum (it is a minimum when
+     the pattern ends in [& rest]).
+
+     No source symbol can contain a [~] — the reader makes it a delimiter — so
+     this name is unspellable and nothing but [Parse] can reach it. *)
+  | "destructure~nth" ->
+    (match args with
+     | [ target;
+         { Ast.e = Ast.Int i; _ }; { Ast.e = Ast.Int n; _ };
+         { Ast.e = Ast.Int exact; _ } ] ->
+       let plural k = if Int64.equal k 1L then "" else "s" in
+       let target = check ctx target in
+       (match target.Tast.ty with
+        | Types.Array (m, elem) ->
+          if Int64.equal exact 1L && not (Int64.equal m n) then
+            fail loc
+              "this pattern binds %Ld name%s, but %s has %Ld element%s — a \
+               pattern over a fixed array names every element, or ends in \
+               [& rest]"
+              n (plural n) (Types.to_string target.Tast.ty) m (plural m);
+          if Int64.equal exact 0L && Int64.compare m n < 0 then
+            fail loc
+              "this pattern binds %Ld name%s before the &, but %s has only %Ld \
+               element%s" n (plural n) (Types.to_string target.Tast.ty) m
+              (plural m);
+          prim Tast.At elem
+            [ target; mk loc index_ty (Tast.Int (i, Types.I32)) ]
+        (* The asymmetry is real and is the reason this is refused rather than
+           lowered to a bounds-checked [at]: a fixed array's length is in its
+           type, so [[a b]] over a [[2 f32]] is a claim the checker can settle,
+           and over a [[T]] it is a claim about a number that does not exist
+           until the program runs. Turning it into a runtime trap would be a
+           pattern that type checks and then kills the program, which is the
+           trade this language does not make. *)
+        | Types.Slice _ ->
+          fail loc
+            "a pattern cannot destructure %s: a slice's length is a runtime \
+             value, so nothing here can check that it has %Ld element%s. Use \
+             (at s i) and test (len s) yourself"
+            (Types.to_string target.Tast.ty) n (plural n)
+        | other ->
+          fail loc
+            "%s is not a fixed array, so [a b ...] cannot destructure it"
+            (Types.to_string other))
+     | _ ->
+       fail loc
+         "destructure~nth is written by the compiler and cannot be called")
+
   (* ── containers ────────────────────────────────────────────────── *)
   | "len" ->
     arity loc name 1 args;
diff --git a/lib/parse.ml b/lib/parse.ml
index 5a8df1d..90fc84a 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -14,6 +14,35 @@ let sym (f : Form.t) =
   | Sym s -> s
   | _ -> fail f "expected a name, found %s" (Form.to_string f)
 
+(* Names for the temporaries a destructuring binding needs — the value is bound
+   once and every name in the pattern reads *that*, so a pattern over a call
+   calls it once. [~] is a delimiter in the reader, so no symbol anyone can
+   write contains one: these cannot collide with a source name and a source
+   name cannot shadow one. Reset per program so the names, and therefore the
+   slot numbering downstream, are the same every run. *)
+let temps = ref 0
+
+let fresh_temp () = incr temps; Printf.sprintf "destructure~%d" !temps
+
+(* Destructuring binds in [let] and nowhere else. Every other binding position —
+   a [defn] parameter, a [defstruct] field, an [fn] parameter, a [dotimes]
+   counter, a [match] arm's binds — takes a plain name, and a pattern written
+   there is refused here rather than falling out of [sym] as "expected a name".
+
+   A parameter is the one worth saying why about: it is a name/type pair, and a
+   pattern has no name to pair the type with, so supporting it means a pattern
+   inside [Ast.field] — a record [Load] and [Shim] both build and read, and
+   neither is this file's to change. *)
+let no_pattern (f : Form.t) =
+  match f.v with
+  | Map _ | Vec _ ->
+    fail f
+      "%s is a destructuring pattern, and a pattern binds only in let — this \
+       position takes a plain name. Take the value under a name and \
+       destructure it in the body"
+      (Form.to_string f)
+  | _ -> ()
+
 (* Primitive type names are lowercase but concrete; every other lowercase name
    in type position is a type variable (plan.org, Types). *)
 let primitives =
@@ -62,6 +91,7 @@ let rec fields (f : Form.t) (items : Form.t list) : Ast.field list =
   match items with
   | [] -> []
   | name :: ty :: rest ->
+    no_pattern name;
     { Ast.fname = sym name; fty = texpr ty; floc = name.loc } :: fields f rest
   | [ odd ] ->
     Loc.fail odd.loc "field %s has no type — these come in name/type pairs"
@@ -166,12 +196,14 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
   | Sym "fn" ->
     (match args with
      | { v = Vec ps; _ } :: body when body <> [] ->
+       List.iter no_pattern ps;
        mk (Ast.Fn (List.map sym ps, body_of body))
      | _ -> fail f "fn is (fn [param ...] body ...)")
 
   | Sym "dotimes" ->
     (match args with
      | { v = Vec [ n; count ]; _ } :: body ->
+       no_pattern n;
        mk (Ast.Dotimes (sym n, expr count, body_of body))
      | _ -> fail f "dotimes is (dotimes [name count] body ...)")
 
@@ -331,15 +363,182 @@ and bindings f (items : Form.t list) : Ast.binding list =
      Annotated locals are not needed by any acceptance program. *)
   let rec go = function
     | [] -> []
-    | name :: value :: rest ->
-      { Ast.bname = sym name; bty = None; bval = expr value; bloc = name.loc }
-      :: go rest
+    | pat :: value :: rest ->
+      let bs = destructure pat (expr value) in
+      no_duplicates pat bs;
+      bs @ go rest
     | [ odd ] ->
       Loc.fail odd.loc "binding %s has no value — let takes name/value pairs"
         (Form.to_string odd)
   in
   if items = [] then Loc.fail f.loc "let needs at least one binding" else go items
 
+(* ── Destructuring ─────────────────────────────────────────────────── *)
+
+(* Clojure's destructuring, desugared here into the bindings and field accesses
+   the language already has. [Ast.binding] carries a name and nothing else, and
+   deliberately so: nothing downstream — not [Load]'s renaming, not [Check], not
+   any backend — learns that a pattern exists. The same reason [dotimes] is a
+   [Let] plus a [While].
+
+   The one thing this cannot decide is whether an array pattern's arity matches
+   the value's, because that is a type and there are none here. [destructure~nth]
+   carries the question to [Check], which answers it and emits an ordinary [at].
+
+   A binding is a pattern only when it is written in brackets or braces; a bare
+   name is what it always was. *)
+and destructure (p : Form.t) (v : Ast.expr) : Ast.binding list =
+  match p.v with
+  | Sym name -> [ { Ast.bname = name; bty = None; bval = v; bloc = p.loc } ]
+  (* The value goes into a temporary first, so it is evaluated once however
+     many names the pattern binds, and so that [(let [{:keys [p]} p] ...)]
+     reads the old [p] rather than the one it is in the middle of rebinding. *)
+  | Map items ->
+    let t = fresh_temp () in
+    { Ast.bname = t; bty = None; bval = v; bloc = p.loc } :: dmap p t items
+  | Vec items ->
+    let t = fresh_temp () in
+    { Ast.bname = t; bty = None; bval = v; bloc = p.loc } :: dvec p t items
+  | _ ->
+    fail p
+      "expected a name or a destructuring pattern, found %s — a pattern is \
+       {:keys [x y]} over a struct or [a b] over a fixed array"
+      (Form.to_string p)
+
+(* {:keys [x y]} and {inner :field}, over a struct. Clojure's map destructuring
+   with Flan's structs standing in for its maps: [:keys] is the common case and
+   the pair form is what nests, since a [:keys] entry is a name and never a
+   pattern. Everything else Clojure puts in this position — [:as], [:or],
+   [:strs], [:syms] — is refused by name where it is written. *)
+and dmap (p : Form.t) (t : string) (items : Form.t list) : Ast.binding list =
+  let ex loc e : Ast.expr = { Ast.e; loc } in
+  let field loc name = ex loc (Ast.Field (ex loc (Ast.Var t), name)) in
+  let rec go = function
+    | [] -> []
+    | { v = Kw "keys"; _ } :: names :: rest ->
+      let ns =
+        match names.v with
+        | Vec ns -> ns
+        | _ ->
+          Loc.fail names.loc
+            ":keys takes a bracketed list of field names, found %s"
+            (Form.to_string names)
+      in
+      let rec each = function
+        | [] -> []
+        | (n : Form.t) :: more ->
+          let name =
+            match n.v with
+            | Sym s -> s
+            | _ ->
+              Loc.fail n.loc
+                ":keys binds field names, and %s is not one — a nested pattern \
+                 is written {%s :field}"
+                (Form.to_string n) (Form.to_string n)
+          in
+          { Ast.bname = name; bty = None; bval = field n.loc name; bloc = n.loc }
+          :: each more
+      in
+      each ns @ go rest
+    | ({ v = Kw k; _ } as bad) :: _ :: rest ->
+      ignore rest;
+      Loc.fail bad.loc
+        ":%s is not implemented in a destructuring pattern — a struct pattern \
+         is {:keys [x y]} or {name :field}, and nothing else" k
+    | pat :: ({ v = Kw fld; _ } as fform) :: rest ->
+      destructure pat (field fform.loc fld) @ go rest
+    | pat :: other :: _ ->
+      Loc.fail other.loc
+        "expected :field after %s, found %s — a struct pattern binds \
+         {name :field}" (Form.to_string pat) (Form.to_string other)
+    | [ odd ] ->
+      Loc.fail odd.loc "%s has no :field — a struct pattern comes in pairs"
+        (Form.to_string odd)
+  in
+  if items = [] then
+    fail p "an empty struct pattern {} binds nothing — write the names it should bind"
+  else go items
+
+(* [a b] and [a b & rest], over a fixed array. Not over a slice: see [Check]. *)
+and dvec (p : Form.t) (t : string) (items : Form.t list) : Ast.binding list =
+  let ex loc e : Ast.expr = { Ast.e; loc } in
+  let var loc n = ex loc (Ast.Var n) in
+  let rec split acc = function
+    | [] -> (List.rev acc, None)
+    | ({ v = Sym "&"; _ } as amp) :: rest ->
+      (match rest with
+       | [ r ] -> (List.rev acc, Some r)
+       | [] -> Loc.fail amp.loc "& needs a name after it, as in [a b & rest]"
+       | _ :: extra :: _ ->
+         Loc.fail extra.loc
+           "& takes one name and it is the last thing in the pattern")
+    | x :: rest -> split (x :: acc) rest
+  in
+  let elems, rest = split [] items in
+  let n = List.length elems in
+  (match elems, rest with
+   | [], None ->
+     fail p "an empty array pattern [] binds nothing — write the names it should bind"
+   | [], Some r ->
+     Loc.fail r.loc
+       "[& %s] binds the whole value — write %s on its own instead of a pattern"
+       (Form.to_string r) (Form.to_string r)
+   | _ -> ());
+  (* With a [& rest] the pattern says "at least this many"; without one it says
+     "exactly this many". [Check] is where the array's length is known, so the
+     count and which of the two it means travel there as arguments. *)
+  let exact = if rest = None then 1L else 0L in
+  let nth i =
+    ex p.loc
+      (Ast.Call (var p.loc "destructure~nth",
+                 [ var p.loc t;
+                   ex p.loc (Ast.Int (Int64.of_int i));
+                   ex p.loc (Ast.Int (Int64.of_int n));
+                   ex p.loc (Ast.Int exact) ]))
+  in
+  let rec each i = function
+    | [] -> []
+    | e :: more -> destructure e (nth i) @ each (i + 1) more
+  in
+  let rest_binding =
+    match rest with
+    | None -> []
+    | Some r ->
+      (* An ordinary (slice t n (len t)): the tail of the temporary, which is a
+         local and outlives the body that reads it. Nothing new. *)
+      let name =
+        match r.v with
+        | Sym s -> s
+        | _ ->
+          Loc.fail r.loc
+            "& binds one name for the tail, and %s is not one — the tail is a \
+             slice, so it cannot be destructured further" (Form.to_string r)
+      in
+      [ { Ast.bname = name; bty = None; bloc = r.loc;
+          bval =
+            ex r.loc
+              (Ast.Call (var r.loc "slice",
+                         [ var r.loc t;
+                           ex r.loc (Ast.Int (Int64.of_int n));
+                           ex r.loc (Ast.Call (var r.loc "len",
+                                               [ var r.loc t ])) ])) } ]
+  in
+  each 0 elems @ rest_binding
+
+(* One pattern binding the same name twice is a mistake, not a shadowing: the
+   second would win and the first would bind nothing. Across a let's bindings it
+   *is* shadowing and stays legal, so this looks at one pattern at a time. *)
+and no_duplicates (p : Form.t) (bs : Ast.binding list) =
+  let rec go seen = function
+    | [] -> ()
+    | (b : Ast.binding) :: rest ->
+      if String.contains b.Ast.bname '~' then go seen rest
+      else if List.mem b.Ast.bname seen then
+        Loc.fail b.Ast.bloc "this pattern binds %s twice" b.Ast.bname
+      else go (b.Ast.bname :: seen) rest
+  in
+  ignore p; go [] bs
+
 and struct_fields f (items : Form.t list) : (string * Ast.expr) list =
   let rec go = function
     | [] -> []
@@ -586,8 +785,9 @@ let declared_types (forms : Form.t list) : Names.t =
 
 let program (forms : Form.t list) : Ast.decl list =
   let types = declared_types forms in
+  temps := 0;
   List.map (decl types) forms
 
 (* Single-declaration entry point, for tests and the REPL. Sees only the
    builtin types plus whatever this one form declares. *)
-let decl (f : Form.t) : Ast.decl = decl (declared_types [ f ]) f
+let decl (f : Form.t) : Ast.decl = temps := 0; decl (declared_types [ f ]) f