diff --git a/TODO.org b/TODO.org
index 7337598d..b13b15df 100644
--- a/TODO.org
+++ b/TODO.org
@@ -10,15 +10,15 @@ pointing at it. A CANCELLED entry carries the one-line reason, because an idea
 rejected without a record is an idea that gets re-proposed.
 
 * Language surface
-** NEXT if let
-Decided 2026-09-26 (126), Rust's spelling: =if let Some(g) = left= plus a block tests
-the pattern and binds =g= in that block only; =elif=/=else= follow as for =if=. Any
-=match= pattern may stand where =Some(g)= is. Reads to a two-arm =match=.
-** NEXT when as a value, and get as a checked lookup
-Decided 2026-09-26 (125): a =when= whose value is used gives =Option(T)=, =Some= of its
-body when the test holds and =None= otherwise; as a statement it is unchanged.
-=get(xs, i, …)= on an array, slice or Vec gives =Option(T)= instead of trapping on an
-index out of range (negative included), one index per dimension. Both typed and dyn.
+** DONE if let
+CLOSED: [2026-09-26]
+=(if-let [P v] then else)= in paren syntax; an elif chain is the else. With no else it
+is a statement, not an Option. Rules out a plain name or =_= as the pattern (use =let=).
+** DONE when as a value, and get as a checked lookup
+CLOSED: [2026-09-26]
+Every one-armed =if= is a =when=; kept, it is =Option(T)=, nested over an Option body
+(Rust's =bool::then=), and body-or-nil where a dyn is wanted. A =_=-inferred return's
+last form is not kept. =get= over dyn text or vec is nil when out of range; =.field= still traps.
 
 ** NEXT str and String
 Decided 2026-09-25: the typed read-only text is =str= (the rename from =string= is
diff --git a/emacs/flan-fln-mode.el b/emacs/flan-fln-mode.el
index ba5f631e..882c0801 100644
--- a/emacs/flan-fln-mode.el
+++ b/emacs/flan-fln-mode.el
@@ -102,7 +102,7 @@ fine here.  Brackets and strings are still paired."
 ;; `header_follow' in lib/indent_reader.ml: the words a statement starts with.
 (defconst flan-fln--header-words
   '("fn" "fn-" "def" "once" "const" "struct" "union" "data" "enum" "import"
-    "if" "elif" "else" "while" "until" "for" "match" "let" "return" "break"
+    "if" "when" "elif" "else" "while" "until" "for" "match" "let" "return" "break"
     "continue" "defer" "handler-case" "handler-bind" "restart-case" "on"
     "restart" "quote" "macro" "type" "class" "generic" "multi" "method"))
 
@@ -111,7 +111,7 @@ fine here.  Brackets and strings are still paired."
 ;; when it is the one-line `fn f(x) = e'; `if' does not when it is the one-line
 ;; `if c then a else b'.
 (defconst flan-fln--opener-words
-  '("fn" "fn-" "struct" "union" "data" "enum" "if" "elif" "else" "while"
+  '("fn" "fn-" "struct" "union" "data" "enum" "if" "when" "elif" "else" "while"
     "until" "for" "match" "defer" "handler-case" "handler-bind"
     "restart-case" "on" "restart" "quote" "macro" "class" "multi" "method"))
 
@@ -409,7 +409,7 @@ and a call ending in `:'."
          (save-excursion
            (goto-char v)
            (or (looking-at "\\(?:match\\|handler-case\\|handler-bind\\|restart-case\\)\\(?:[ \t]\\|$\\)")
-               (and (looking-at "if[ \t]") (not (flan-fln--then l)))
+               (and (looking-at "\\(?:if\\|when\\)[ \t]") (not (flan-fln--then l)))
                (flan-fln--lambda-header-p v end))))))
 
 ;;; Statements
@@ -1250,7 +1250,7 @@ Before it at the same level, else out to the line that owns this block."
                  (not (save-excursion
                         (goto-char w-end)
                         (looking-at "[ \t]+[^][ \t\n(){},;\":]+("))))
-                ((member w '("if" "elif")) (not (flan-fln--then start)))
+                ((member w '("if" "when" "elif")) (not (flan-fln--then start)))
                 (t t)))))
       ;; `let r = match n', `x = if c', `fn f(x) = match x', a lambda
       ;; header: the value goes on under the line.
@@ -1758,6 +1758,9 @@ lambda or a `Fn(...)' type, and not after a match arm's."
     ;; The words inside a line: `for i in range(n)', `if c then a else b', a
     ;; `where' constraint.
     ("[ \t]\\(then\\|else\\|in\\|where\\)[ \t]" 1 font-lock-keyword-face)
+    ;; `if let Some(g) = x', and a value's `if' or `when', `x = when c then a'.
+    ("\\_<if[ \t]+\\(let\\)[ \t]" 1 font-lock-keyword-face)
+    ("[ \t=(,]\\(if\\|when\\)[ \t]" 1 font-lock-keyword-face)
     ;; The operator words.
     ("\\_<\\(and\\|or\\|not\\)\\_>" 1 font-lock-keyword-face)
     (,(concat "\\_<" (regexp-opt flan--constants t) "\\_>")
diff --git a/emacs/flan-mode.el b/emacs/flan-mode.el
index 4e0d3b30..b7bfafbc 100644
--- a/emacs/flan-mode.el
+++ b/emacs/flan-mode.el
@@ -128,7 +128,7 @@
   "Forms that introduce a top-level name.")
 
 (defconst flan--special
-  '("quote" "do" "let" "if" "when" "cond" "and" "or"
+  '("quote" "do" "let" "if" "if-let" "when" "cond" "and" "or"
     "while" "until" "break" "continue" "return" "set"
     "array" "array-fill" "array-gen" "the" "match" "fn" "dotimes" "loop" "recur"
     "defer" "some" "try" "signal" "error"
@@ -580,6 +580,7 @@ For `syntax-propertize-function'."
     ("handler-case" . 1)
     ;; Test first, body after.
     ("if" . 1)
+    ("if-let" . 1)
     ("when" . 1)
     ("unless" . 1)
     ("while" . 1)
diff --git a/emacs/test-flan-fln.el b/emacs/test-flan-fln.el
index 1a36cefe..6af0b925 100644
--- a/emacs/test-flan-fln.el
+++ b/emacs/test-flan-fln.el
@@ -858,6 +858,20 @@ defconst(k, 3)
                    (test-flan-fln--tabs "let colors =\n|" 1) 2)
 (test-flan-fln--is "but not after a one-line fn"
                    (test-flan-fln--tabs "fn f() -> i32 = 1\n|" 1) 0)
+(test-flan-fln--is "after if let, one level deeper"
+                   (test-flan-fln--tabs "fn f() -> ()\n  if let Some(g) = o\n|" 1) 4)
+(test-flan-fln--is "and after a when with a block"
+                   (test-flan-fln--tabs "fn f() -> ()\n  when a > 1\n|" 1) 4)
+(test-flan-fln--is "but not after a one-line when"
+                   (test-flan-fln--tabs "fn f() -> ()\n  when a then b()\n|" 1) 2)
+(test-flan-fln--in "fn f() -> ()\n  if let Some(g) = o\n    g\n  let w = when a then 1\n  when b\n    c()\n"
+  (font-lock-ensure)
+  (let ((face (lambda (needle)
+                (save-excursion (goto-char (point-min)) (search-forward needle)
+                                (get-text-property (match-beginning 0) 'face)))))
+    (test-flan-fln--is "if let's let is a keyword" (funcall face "let Some") 'font-lock-keyword-face)
+    (test-flan-fln--is "a value's when is a keyword" (funcall face "when a") 'font-lock-keyword-face)
+    (test-flan-fln--is "and so is a statement's" (funcall face "when b") 'font-lock-keyword-face)))
 (test-flan-fln--is "else goes to its if's column, whatever the depth"
                    (test-flan-fln--tabs "if a\n  if b\n    c\n      |else" 1) 2)
 (test-flan-fln--is "and a second TAB to the outer if's"
diff --git a/lib/ast.ml b/lib/ast.ml
index 8850fd71..cb55e80e 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -79,6 +79,10 @@ and expr_kind =
   | Field  of expr * string           (* (.pos c) — auto-derefs one level *)
   | Call   of expr * expr list
   | Match  of expr * arm list
+  (* (if-let [(Some g) left] then else) — [if let Some(g) = left] in .fln.
+     A two-arm [match]: the arm is the pattern with [then] as its body, and
+     the else is the [_] arm. With no else it is a statement. *)
+  | IfLet  of expr * arm * expr option
   | Struct of string * (string * expr) list   (* (Cursor {.src s}) *)
   (* {.src s .pos 0} with no type written in front of it. The fields alone do
      not name a type, so this node carries no name and is only checkable where
@@ -465,6 +469,7 @@ let map_children f (e : expr) : expr =
     | Field (x, n) -> Field (ex x, n)
     | Call (fn, args) -> Call (ex fn, List.map ex args)
     | Match (s, arms) -> Match (ex s, List.map arm arms)
+    | IfLet (s, a, e) -> IfLet (ex s, arm a, Option.map ex e)
     | Struct (n, fs) -> Struct (n, List.map (fun (n, v) -> (n, ex v)) fs)
     | Bare fs -> Bare (List.map (fun (n, v) -> (n, ex v)) fs)
     | MapLit (tag, kvs) -> MapLit (tag, List.map (fun (k, v) -> (ex k, ex v)) kvs)
@@ -538,6 +543,8 @@ and step_expr fn (e : expr) : expr =
   | Dotimes (l, n, b, es) -> { e with e = Dotimes (l, n, b, step_body fn es) }
   | Match (sc, arms) ->
     { e with e = Match (sc, List.map (fun a -> { a with body = step_body fn a.body }) arms) }
+  | IfLet (sc, a, b) ->
+    { e with e = IfLet (sc, { a with body = step_body fn a.body }, Option.map branch b) }
   | _ -> e
 
 let instrument_step ?(fn = "step-point") (ds : decl list) : decl list option =
diff --git a/lib/check.ml b/lib/check.ml
index aa7423a1..f9aecd2f 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -863,6 +863,13 @@ type ctx = {
      and a [match] arm. Everything else is therefore non-tail by construction,
      and no walk has to enumerate the cases that are not. *)
   mutable tail : bool;
+  (* True where this form's value is kept: a [let] binding's value, and what
+     a block's last form, an [if]'s arms and a [match]'s arms inherit from
+     the form they stand in. Read and withdrawn at the top of [check] as
+     [tail] is. Only a one-armed [if] ([when]) asks: used, it answers an
+     Option; not, it is a statement. [want] alone cannot say, since a
+     statement and an unannotated [let] value both arrive with none. *)
+  mutable used : bool;
   (* True inside a [defer]'s forms. A defer is the cleanup a transfer runs on
      its way out (§5), so a transfer *starting* there has no answer: this
      function's defers are already half run and the first transfer's target is
@@ -4780,7 +4787,7 @@ let with_recovery env ~on f =
 
 let invented_ctx env ret =
   { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
-    defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
+    defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false; used = false;
     in_defer = false; defer_ok = false; defer_block = "a nested form";
     owner = "<none>" }
 
@@ -5428,7 +5435,8 @@ let truthy_depth = ref 0
    it — the square of a refused or/and chain's length. *)
 let if_failed :
   (Loc.t,
-   Ast.expr * ((string * binding) list * Types.t) * Types.t option * Loc.diag)
+   Ast.expr * ((string * binding) list * Types.t) * (Types.t option * bool)
+   * Loc.diag)
     Hashtbl.t =
   Hashtbl.create 16
 let if_depth = ref 0
@@ -5657,6 +5665,8 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
      it unless the arm below hands it on deliberately. *)
   let tail = ctx.tail in
   ctx.tail <- false;
+  let used = ctx.used in
+  ctx.used <- false;
   match e.Ast.e with
   (* A negative literal in a generic body, at an instantiation that made it
      unsigned. The cast the ordinary refusal names would be wrong at every
@@ -5837,13 +5847,13 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
     in
     check ctx ?want { e with Ast.e = Ast.Int n }
   | Ast.Var name -> var ctx loc ~want name
-  | Ast.Do body -> ctx.tail <- tail; block ctx ?want loc body
+  | Ast.Do body -> ctx.tail <- tail; ctx.used <- used; block ctx ?want loc body
   (* [defer_ok] rides through: a [let] at the top level of a function body has
      exactly the function's extent, and so does a [let] nested inside one.
      [tail] rides through for the same shape of reason: a [recur] written as
      the last form of a [let] inside a loop body is in the loop's tail. *)
-  | Ast.Let (bs, body) -> check_let ctx ~tail ?want ~defer_ok loc bs body
-  | Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e'
+  | Ast.Let (bs, body) -> check_let ctx ~tail ~used ?want ~defer_ok loc bs body
+  | Ast.If (c, t, e') -> check_if ctx ~tail ~used ?want loc c t e'
   | Ast.While (label, c, body) ->
     (* The condition is part of the loop even though it is written outside the
        braces — emit puts it in the header block, so it is re-evaluated at the
@@ -6039,7 +6049,9 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.ArrayFill (dims, v) -> check_array_fill ctx ~want loc dims v
   | Ast.ArrayGen (dims, f) -> check_array_gen ctx ~want loc dims f
   | Ast.The (t, v) -> check_the ctx ~want loc t v
-  | Ast.Match (scrutinee, arms) -> check_match ctx ~tail ?want loc scrutinee arms
+  | Ast.Match (scrutinee, arms) -> check_match ctx ~tail ~used ?want loc scrutinee arms
+  | Ast.IfLet (scrutinee, arm, els) ->
+    check_if_let ctx ~tail ~used ?want loc scrutinee arm els
   (* Constant integer arithmetic where a type variable is wanted is folded to
      the literal it computes first, so [(+ x (+ 1 2))] is admitted wherever
      [(+ x 3)] is. The instantiation re-checks the form unfolded, at a concrete
@@ -6463,20 +6475,24 @@ and block ctx ?want ?(defer_ok = false) loc body =
   match body with
   (* Withdrawn here too. An empty body has no last form to be the tail, so
      leaving the permission set would hand it to whatever is checked next. *)
-  | [] -> ctx.tail <- false; expect ctx loc ~want (unit_at loc)
+  | [] -> ctx.tail <- false; ctx.used <- false; expect ctx loc ~want (unit_at loc)
   | _ ->
     (* A block's tail is its last form and nothing else. Callers that must not
        pass one on need do nothing: [check] withdrew it before they were
        reached, so [tail] is already false here for all of them. *)
     let tail = ctx.tail in
+    let used = ctx.used in
+    ctx.used <- false;
     let rec go = function
       | [ last ] ->
         ctx.defer_ok <- defer_ok;
         ctx.tail <- tail;
+        ctx.used <- used;
         let l = check ctx ?want last in [ l ], l.Tast.ty
       | x :: rest ->
         ctx.defer_ok <- defer_ok;
         ctx.tail <- false;
+        ctx.used <- false;
         let x = check ctx x in
         let rest, ty = go rest in x :: rest, ty
       | [] -> assert false
@@ -7090,12 +7106,13 @@ and defer_counter_zero slot loc =
 (* [defer_ok] says whether *this* let has the function's extent. If it does, so
    does every form in its body, including a nested let — which is why the flag
    is handed to the body rather than consumed here. *)
-and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
+and check_let ctx ?(tail = false) ?(used = false) ?want ?(defer_ok = false) loc bs body =
   scoped ctx (fun () ->
     let bs =
       map_lr
         (fun (b : Ast.binding) ->
            let want = Option.map (resolve ctx.env) b.Ast.bty in
+           ctx.used <- true;
            let v = check ctx ?want b.Ast.bval in
            (match v.Tast.ty with
             (* A refused initialiser, already reported: the name is bound to
@@ -7112,6 +7129,7 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
     in
     (* After the bindings, because checking each of them withdrew it. *)
     ctx.tail <- tail;
+    ctx.used <- used;
     let body = block ctx ?want ~defer_ok loc body in
     mk loc body.Tast.ty (Tast.Let (bs, [ body ])))
 
@@ -7583,14 +7601,14 @@ and check_truthy_once ctx c =
      with Loc.Error d -> refuse_or_poison ctx.env loc d))
   | exception Loc.Error _ -> check ctx ~want:Types.Bool c
 
-and check_if ctx ?(tail = false) ?want loc c t e =
+and check_if ctx ?(tail = false) ?(used = false) ?want loc c t e =
   if ctx.env.recovering && ctx.env.speculating = 0 then
-    check_if_once ctx ~tail ?want loc c t e
+    check_if_once ctx ~tail ~used ?want loc c t e
   else
   match
     List.find_opt
       (fun (n, (sc, r), w, _) ->
-         n == c && r == ctx.ret && w = want && same_scope sc ctx.scope)
+         n == c && r == ctx.ret && w = (want, used) && same_scope sc ctx.scope)
       (Hashtbl.find_all if_failed c.Ast.loc)
   with
   | Some (_, _, _, d) -> raise (Loc.Error d)
@@ -7602,23 +7620,20 @@ and check_if ctx ?(tail = false) ?want loc c t e =
           decr if_depth;
           if !if_depth = 0 then Hashtbl.reset if_failed)
       (fun () ->
-         try check_if_once ctx ~tail ?want loc c t e
+         try check_if_once ctx ~tail ~used ?want loc c t e
          with Loc.Error d as ex ->
-           Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d);
+           Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), (want, used), d);
            raise ex)
 
-and check_if_once ctx ~tail ?want loc c t e =
+and check_if_once ctx ~tail ~used ?want loc c t e =
   let c = check_truthy ctx c in
   (* Both arms are the tail, and a one-armed [if] counts: [(when c (recur ...))]
      is how nearly every loop is written, and the branch is still the last
-     thing the body does. *)
-  let in_tail f = ctx.tail <- tail; f () in
+     thing the body does. Both arms are kept when the [if] is. *)
+  let in_tail f = ctx.tail <- tail; ctx.used <- used; f () in
   match e with
-  | None ->
-    (* A one-armed if produces Unit whatever the branch evaluates to: there is
-       no value on the missing side. `when` desugars to this. *)
-    let t = branch ctx (fun () -> in_tail (fun () -> check ctx t)) in
-    expect ctx loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
+  | None -> check_when ctx ~used ?want loc c (fun ?want () ->
+      branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)))
   (* Two literal arms meet at the wider of their own types, as two literal
      elements of an array do: [(if c 1 2.5)] is an f64. *)
   | Some e
@@ -7813,6 +7828,48 @@ and check_if_once ctx ~tail ?want loc c t e =
     in
     mk loc ty (Tast.If (c, t, e))
 
+(* A one-armed [if], which [when] is. As a statement it is Unit whatever its
+   branch evaluates to. Kept — a [let]'s value, an argument, a return, or
+   anything else with a type wanted of it — it answers (Option T): [Some] of
+   the branch when the test held and [None] when it did not. A branch that
+   is already an Option is not flattened: the answer is (Option (Option T)),
+   Rust's [bool::then], so [None] from the branch and a failed test stay two
+   answers.
+
+   Dyn has no Option. Where a dyn is wanted, or the branch is a dyn, a false
+   test answers nil and a true one the branch's value — one absence, as a
+   dyn map's [get] has.
+
+   A branch with no value (Unit) or none at all (Never) keeps the statement's
+   Unit, so what is refused about binding one is refused as before. *)
+and check_when ctx ~used ?want loc c
+    (branch_at : ?want:Types.t -> unit -> Tast.expr) =
+  let stmt t = expect ctx loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc))) in
+  let nil () = rt loc Types.Dyn "flan_dyn_nil" [] in
+  let valueless (t : Tast.expr) =
+    match t.Tast.ty with Types.Unit | Types.Never -> true | _ -> false
+  in
+  match want with
+  | Some (Types.Unit | Types.Never) -> stmt (branch_at ())
+  | Some Types.Dyn ->
+    let t = branch_at ~want:Types.Dyn () in
+    mk loc Types.Dyn (Tast.If (c, t, nil ()))
+  | Some (Types.Option inner) ->
+    let t = branch_at ~want:inner () in
+    let oty = Types.Option inner in
+    let some = if t.Tast.ty = Types.Never then t else mk loc oty (Tast.Some_ t) in
+    mk loc oty (Tast.If (c, some, mk loc oty Tast.None_))
+  | None when not used -> stmt (branch_at ())
+  | _ ->
+    let t = branch_at () in
+    if valueless t then stmt t
+    else if Types.equal t.Tast.ty Types.Dyn then
+      expect ctx loc ~want (mk loc Types.Dyn (Tast.If (c, t, nil ())))
+    else
+      let oty = Types.Option t.Tast.ty in
+      expect ctx loc ~want
+        (mk loc oty (Tast.If (c, mk loc oty (Tast.Some_ t), mk loc oty Tast.None_)))
+
 (* The type two literals meet at, each at its own type — a wide integer at
    u64, which is the only type that holds one. *)
 and literal_join ctx (a : Ast.expr) (b : Ast.expr) =
@@ -8856,7 +8913,12 @@ and check_array_gen ctx ~want loc dims f =
     (array_build ctx loc ns elem ~pre:[ (fs, f) ]
        ~element:(fun idxs -> mk loc elem (Tast.CallPtr (fv, idxs))))
 
-and check_match ctx ?(tail = false) ?want loc scrutinee arms =
+and check_match ctx ?(tail = false) ?(used = false) ?(stmt = false) ?want loc
+    scrutinee arms =
+  (* [stmt] is an [if let] with no else: a statement, Unit whatever its arm
+     answers, as a one-armed [if] is when nothing keeps it. *)
+  let used = used && not stmt in
+  let want = if stmt then None else want in
   let s = check ctx scrutinee in
   (* What the arms are alternatives over. An [Option] is a two-case data type
      wearing a special coat, so the two shapes below are the same shape: a set
@@ -9260,6 +9322,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
            (* Every arm is the tail, exactly as an [if]'s two arms are.
               Restored here because checking the scrutinee withdrew it. *)
            ctx.tail <- tail;
+           ctx.used <- used;
            let arm = (a, ctor, binds) in
            let body =
              if free && !want <> None && not (literal_arm arm) then
@@ -9306,7 +9369,12 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
                   | Error _ -> at !want ())
              else block ctx ?want:!want a.Ast.aloc a.Ast.body
            in
-           (if body.Tast.ty <> Types.Never then
+           let body =
+             if stmt && body.Tast.ty <> Types.Unit && body.Tast.ty <> Types.Never
+             then mk body.Tast.loc Types.Unit (Tast.Do [ body; unit_at body.Tast.loc ])
+             else body
+           in
+           (if body.Tast.ty <> Types.Never && not stmt then
               match !want with
               | None -> want := Some body.Tast.ty
               | Some w when free ->
@@ -9400,7 +9468,10 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
       (String.concat ", " missing)
       (if List.length missing = 1 then "has" else "have")
       (if List.length missing = 1 then "it" else "them");
-  let ty = match !want with Some t -> t | None -> Types.Never in
+  let ty =
+    if stmt then Types.Unit
+    else match !want with Some t -> t | None -> Types.Never
+  in
   match subject with
   | `Option _ | `Data _ -> mk loc ty (Tast.Match (s, arms))
   | `Enum _ | `Bool | `Lit _ ->
@@ -9436,6 +9507,49 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
     in
     mk loc ty (Tast.Let ([ (slot, s) ], [ chain arms ]))
 
+(* [if let P = v] — (if-let [P v] then else) — is the two-arm match
+   [(match v P then _ else)]. With no else it is a statement, Unit whatever
+   [then] answers, as a one-armed [if] is.
+
+   A pattern that cannot fail — [_], or a plain name, which is a name to bind
+   and not a case — tests nothing, and is refused toward [let]. A bare name is
+   a case when some data type, Option or bool has a case of that name, or it
+   names an enum member through its enum. *)
+and check_if_let ctx ~tail ~used ?want loc scrutinee (arm : Ast.arm) els =
+  let fln = fln_source loc in
+  let is_case n =
+    List.mem n [ "None"; "Some"; "true"; "false" ]
+    || String.contains n '.'
+    || Hashtbl.fold
+         (fun _ u acc -> acc || Tast.case_index u n <> None)
+         ctx.env.datas false
+  in
+  let irrefutable name =
+    match name with
+    | Some n ->
+      Loc.failk "check/if-let-irrefutable" arm.Ast.aloc
+        "the pattern %s is a plain name, which always matches, so this if let \
+         has nothing to test. Bind the value with %s"
+        n
+        (if fln then Printf.sprintf "let %s = ..." n
+         else Printf.sprintf "(let [%s ...] ...)" n)
+    | None ->
+      Loc.failk "check/if-let-irrefutable" arm.Ast.aloc
+        "the pattern _ always matches, so this if let has nothing to test. \
+         Use the value directly, or match on it"
+  in
+  (match arm.Ast.pat with
+   | Ast.Pwild -> irrefutable None
+   | Ast.Pctor (n, []) when not (is_case n) -> irrefutable (Some n)
+   | _ -> ());
+  let wild body = { Ast.pat = Ast.Pwild; body; aloc = loc } in
+  match els with
+  | Some e ->
+    check_match ctx ~tail ~used ?want loc scrutinee [ arm; wild [ e ] ]
+  | None ->
+    expect ctx loc ~want
+      (check_match ctx ~tail ~stmt:true loc scrutinee [ arm; wild [] ])
+
 (* ── Places ────────────────────────────────────────────────────────── *)
 
 (* The fields a name has, whether it is a struct or an untagged union. The two
@@ -10702,6 +10816,141 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
     fail loc
       "a Vec takes exactly one index, as (at v i)"
 
+(* [(get xs i ...)] over an array, a slice, a string or a Vec: the element
+   as [(Some e)], or [None] when any index is out of range, negative
+   included, where [at] would trap. One index per dimension, as [at] takes.
+
+   The indices are evaluated once, left to right, before any test. An array's
+   length is static, so the array itself is read once and is not copied; a
+   slice's, a string's or a Vec's is read off the value, so that value is
+   put in a slot first unless it is already a name. Each level is tested
+   before the next is reached, because a Vec of Vecs has no inner length to
+   test until the outer index is known to be in range. The element is then
+   read by [at] as usual, whose own check can no longer fail. *)
+and checked_get ctx ~want loc (target : Tast.expr) (idx : Ast.expr list) =
+  let rec result ty = function
+    | [] -> ty
+    | (i : Ast.expr) :: rest ->
+      (match ty with
+       | Types.Array (_, t) | Types.Slice (_, t) | Types.Vec t -> result t rest
+       | Types.String -> result (Types.Int Types.U8) rest
+       | other ->
+         fail i.Ast.loc
+           "get takes an array, a slice, a string, a Vec, a Map or a dyn, and \
+            %s cannot be indexed" (tyname i.Ast.loc other))
+  in
+  let oty = Types.Option (result target.Tast.ty idx) in
+  let none () = mk loc oty Tast.None_ in
+  let is_name (e : Tast.expr) =
+    match e.Tast.e with Tast.Local _ | Tast.Global _ -> true | _ -> false
+  in
+  (* A value a call answered is bound before the indices run, so the target
+     is still evaluated first. *)
+  let pre = ref [] in
+  let target =
+    match target.Tast.e with
+    | Tast.Call _ | Tast.CallPtr _ ->
+      let s = fresh_slot ctx target.Tast.ty in
+      pre := [ (s, target) ];
+      mk loc target.Tast.ty (Tast.Local s)
+    | _ -> target
+  in
+  let islots =
+    map_lr
+      (fun (i : Ast.expr) ->
+         let v = index_expr ctx i in
+         let s = fresh_slot ctx index_ty in
+         (s, v))
+      idx
+  in
+  let ivar (s, _) = mk loc index_ty (Tast.Local s) in
+  let i32 k = mk loc index_ty (Tast.Int (k, Types.I32)) in
+  let within i len =
+    let ge = mk loc Types.Bool (Tast.Prim (Tast.Ge, [ i; i32 0L ])) in
+    let lt = mk loc Types.Bool (Tast.Prim (Tast.Lt, [ i; len ])) in
+    mk loc Types.Bool (Tast.If (ge, lt, mk loc Types.Bool (Tast.Bool false)))
+  in
+  (* The value reached so far is [base] indexed by [path], innermost last. *)
+  let reached base path ty =
+    if path = [] then base
+    else mk loc ty (Tast.Prim (Tast.At, base :: List.rev path))
+  in
+  (* A value whose length is read as well as indexed, in a slot unless it is
+     a name already. *)
+  let named cur k =
+    if is_name cur then k cur
+    else
+      let s = fresh_slot ctx cur.Tast.ty in
+      mk loc oty
+        (Tast.Let ([ (s, cur) ], [ k (mk loc cur.Tast.ty (Tast.Local s)) ]))
+  in
+  let rec go base path ty = function
+    | [] -> mk loc oty (Tast.Some_ (reached base path ty))
+    | i :: rest ->
+      let i = ivar i in
+      (match ty with
+       | Types.Array (n, t) ->
+         mk loc oty (Tast.If (within i (i32 n), go base (i :: path) t rest, none ()))
+       | Types.Slice _ | Types.String ->
+         let t =
+           match ty with Types.Slice (_, t) -> t | _ -> Types.Int Types.U8
+         in
+         named (reached base path ty) (fun cur ->
+             let len = mk loc index_ty (Tast.Prim (Tast.Len, [ cur ])) in
+             mk loc oty (Tast.If (within i len, go cur [ i ] t rest, none ())))
+       | Types.Vec t ->
+         named (reached base path ty) (fun cur ->
+             let n = rt loc (Types.Int Types.I64) "flan_vec_len" [ cur; here loc ] in
+             let len = mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])) in
+             let p =
+               rt loc (Types.Ptr (Types.Mut, t)) "flan_vec_at"
+                 [ cur; i; size_of loc t; here loc ]
+             in
+             mk loc oty
+               (Tast.If (within i len, go (mk loc t (Tast.Deref p)) [] t rest,
+                         none ())))
+       | _ -> assert false)
+  in
+  expect ctx loc ~want
+    (mk loc oty (Tast.Let (!pre @ islots, [ go target [] target.Tast.ty islots ])))
+
+(* [(get d k ...)] over a dyn: a map's value at the key, a vec's or a text's
+   element at the index, or nil when there is none — dyn has no Option. More
+   than one key walks a level per key, and a nil level answers nil. *)
+and dyn_get ctx ~want loc (target : Tast.expr) (keys : Ast.expr list) =
+  let nil () = rt loc Types.Dyn "flan_dyn_nil" [] in
+  let one v k = rt loc Types.Dyn "flan_dyn_get_at" [ v; k; here loc ] in
+  let keys =
+    map_lr
+      (fun k -> (fresh_slot ctx Types.Dyn, check ctx ~want:Types.Dyn k))
+      keys
+  in
+  let kvar (s, _) = mk loc Types.Dyn (Tast.Local s) in
+  let rec go v = function
+    | [] -> v
+    | k :: rest when rest = [] -> one v (kvar k)
+    | k :: rest ->
+      let s = fresh_slot ctx Types.Dyn in
+      let sv = mk loc Types.Dyn (Tast.Local s) in
+      let is_nil =
+        mk loc Types.Bool
+          (Tast.Prim (Tast.Ne,
+                      [ rt loc (Types.Int Types.I32) "flan_dyn_is_nil" [ sv ];
+                        mk loc (Types.Int Types.I32) (Tast.Int (0L, Types.I32)) ]))
+      in
+      mk loc Types.Dyn
+        (Tast.Let ([ (s, one v (kvar k)) ],
+                   [ mk loc Types.Dyn (Tast.If (is_nil, nil (), go sv rest)) ]))
+  in
+  match keys with
+  | [ (_, k) ] -> expect ctx loc ~want (one target k)
+  | _ ->
+    let ts = fresh_slot ctx Types.Dyn in
+    expect ctx loc ~want
+      (mk loc Types.Dyn
+         (Tast.Let ((ts, target) :: keys,
+                    [ go (mk loc Types.Dyn (Tast.Local ts)) keys ])))
+
 (* [(slice v)], [(slice v lo)] and [(slice v lo hi)] over a Vec — the arm for
    it is in [slice], and this is the half that differs from an array's.
 
@@ -11932,20 +12181,29 @@ and named_call ?(qualified = false) ctx ~want loc name args =
      There is no allocation here and therefore no guard: a lookup that finds
      nothing is an answer, not a failure. *)
   | "get" ->
-    arity ctx loc name 2 args;
     (match args with
+     | target :: (_ :: _ :: _ as idx) ->
+       (* Two indices or more: an array, a slice or a Vec, one per
+          dimension, or a dyn walked a level per index. A map takes one key. *)
+       let target = check_target ctx target in
+       (match target.Tast.ty with
+        | Types.Map _ ->
+          fail loc "a map's get takes one key, as (get m k), and this has %d"
+            (List.length idx)
+        | Types.Dyn -> dyn_get ctx ~want loc target idx
+        | _ -> checked_get ctx ~want loc target idx)
      | [ target; k ] ->
        let target = check_target ctx target in
+       (match target.Tast.ty with
+        | Types.Array _ | Types.Slice _ | Types.String | Types.Vec _ ->
+          checked_get ctx ~want loc target [ k ]
+        | Types.Dyn -> dyn_get ctx ~want loc target [ k ]
+        | _ ->
        (* A dyn map's absence is nil, not None: the typed map can promise an
           (Option V) because V was written down, and a dyn map has nothing to
           write. nil is an ordinary dyn value the caller compares against —
           and (contains? m k) is the question to ask when nil might also be
           stored under the key. *)
-       if target.Tast.ty = Types.Dyn then
-         expect ctx loc ~want
-           (rt loc Types.Dyn "flan_dyn_get"
-              [ target; check ctx ~want:Types.Dyn k; here loc ])
-       else begin
        let kt, vt = map_kv loc "get" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred, and the placeholder is [None] rather than [Unit]: this
@@ -11954,9 +12212,8 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        if deferred_key ctx.env loc "get" kt then
          expect ctx loc ~want (mk loc (Types.Option vt) Tast.None_)
        else
-       map_lookup ctx ~want loc "flan_map_get" target kt vt k
-       end
-     | _ -> assert false)
+       map_lookup ctx ~want loc "flan_map_get" target kt vt k)
+     | _ -> arity ctx loc name 2 args; assert false)
 
   (* (keyword s) -> the interned dyn keyword named by the bytes, for a name
      that only exists at run time — a reader building :texture-path out of a
@@ -14216,7 +14473,7 @@ and trial ctx f =
   let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
                        defers; defer_slot; defer_ok; defer_block; outer = _;
                        outer_what; caught; place_ok; envslot; parent = _;
-                       in_frames; loops; tail; in_defer;
+                       in_frames; loops; tail; used; in_defer;
                        owner = _ } = ctx in
   let undo, keep = snapshot_env ctx.env in
   match speculate ctx.env f with
@@ -14229,7 +14486,8 @@ and trial ctx f =
     ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
     ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
     ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot;
-    ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
+    ctx.loops <- loops; ctx.tail <- tail; ctx.used <- used;
+    ctx.in_defer <- in_defer;
     Error d
   | exception e -> keep (); raise e
 
@@ -14590,10 +14848,13 @@ let builtins : (string * string * string) list =
     ("put", "put [(Map K V) K V] ()",
      "Inserts or replaces. Unit rather than an error code, and \
       (set (get m k) v) is not map syntax.");
-    ("get", "get [(Map K V) K] (Option V)",
+    ("get", "get [(Map K V) K]|[collection i32 ...] (Option V)|(Option T)",
      "The value at the key, or None. Nothing signals here — a lookup that \
       finds nothing is an answer — and the value comes back as a copy of \
-      its bytes.");
+      its bytes. Over an array, a slice, a string or a Vec it is at that \
+      answers None for an index out of range, negative included, one index \
+      per dimension. Over a dyn it answers nil for an absent key or index, \
+      and more keys walk a level each.");
     ("map-remove", "map-remove [(Map K V) K] (Option V)",
      "Removes the entry and answers the value it held, or None if there was \
       none.");
@@ -15597,6 +15858,9 @@ let escaping_names ~returns (body : Ast.expr list) : string list =
     | Ast.Do es | Ast.Let (_, es) ->
       (match List.rev es with x :: _ -> tails x | [] -> ())
     | Ast.If (_, a, b) -> tails a; Option.iter tails b
+    | Ast.IfLet (_, a, b) ->
+      (match List.rev a.Ast.body with x :: _ -> tails x | [] -> ());
+      Option.iter tails b
     | Ast.Match (_, arms) ->
       List.iter
         (fun (a : Ast.arm) ->
diff --git a/lib/emit.ml b/lib/emit.ml
index 97240c6e..e003b8f4 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -5021,6 +5021,7 @@ declare void @flan_dyn_class_hook(ptr)
 declare i64 @flan_dyn_kw(ptr, i64)
 declare i64 @flan_dyn_map_get(i64, i64)
 declare i64 @flan_dyn_get(i64, i64, ptr, i64)
+declare i64 @flan_dyn_get_at(i64, i64, ptr, i64)
 declare void @flan_dyn_map_set(i64, i64, i64)
 declare i64 @flan_dyn_map_contains(i64, i64)
 declare i64 @flan_dyn_map_contains_at(i64, i64, ptr, i64)
diff --git a/lib/indent_printer.ml b/lib/indent_printer.ml
index 62325b7a..8c991e88 100644
--- a/lib/indent_printer.ml
+++ b/lib/indent_printer.ml
@@ -432,8 +432,19 @@ and list f h args =
     ("fn(" ^ commas ps ^ ") => " ^ unit_text body, 0)
   | Form.Sym "if", [ c; a; b ] ->
     ("if " ^ at 1 c ^ " then " ^ inline_text ~lvl:1 a ^ " else " ^ inline_text b, 0)
+  (* A used when is a value, [when c then a]. *)
+  | Form.Sym "when", [ c; a ] -> ("when " ^ at 1 c ^ " then " ^ inline_text a, 0)
+  | Form.Sym "if-let", ({ v = Form.Vec [ _; _ ]; _ } as hd) :: a :: ([] | [ _ ] as b) ->
+    (if_let_head hd ^ " then " ^ inline_text ~lvl:1 a
+     ^ (match b with [ b ] -> " else " ^ inline_text b | _ -> ""), 0)
   | _ -> call ()
 
+(* [if let P = v], the head (if-let [P v] ...) is written with. *)
+and if_let_head (hd : Form.t) =
+  match hd.v with
+  | Form.Vec [ pat; v ] -> "if let " ^ at 8 pat ^ " = " ^ at 1 v
+  | _ -> assert false
+
 (* A one-line slot's text — an arm's value, a then or an else, what follows
    defer: the statements that fit on a line are written as statements,
    everything else as a value. [lvl] is what a value in the slot needs. *)
@@ -595,7 +606,7 @@ let body_guess (h : Form.t) args =
        let stmt_like (a : Form.t) =
          match a.v with
          | Form.List ({ v = Form.Sym h; _ } :: _) ->
-           List.mem h [ "let"; "set"; "when"; "unless"; "cond"; "while";
+           List.mem h [ "let"; "set"; "when"; "if-let"; "unless"; "cond"; "while";
                         "until"; "dotimes"; "match"; "handler-case";
                         "handler-bind"; "restart-case"; "return"; "defer";
                         "do"; "break"; "continue" ]
@@ -666,7 +677,7 @@ let body_split (h : Form.t) args =
   | Some k, _ -> Some (k, false)
 
 let sugar_heads =
-  [ "let"; "set"; "if"; "when"; "cond"; "while"; "until"; "dotimes"; "match";
+  [ "let"; "set"; "if"; "when"; "if-let"; "cond"; "while"; "until"; "dotimes"; "match";
     "handler-case"; "handler-bind"; "restart-case"; "return"; "defer"; "do";
     "quasiquote"; "update" ]
 
@@ -978,6 +989,49 @@ and sugar n (f : Form.t) : string list option =
          @ [ Source_text.tag b.loc.Loc.line (i ^ "else") ] @ slot (n + 2) b)
   | Form.List ({ v = Form.Sym "when"; _ } :: c :: (_ :: _ as body)) ->
     Some ((i ^ "if " ^ at 1 c) :: block (n + 2) body)
+  (* [if let P = v] and its block; an else that is a cond is its elif
+     chain, which is what the reader makes of one. *)
+  | Form.List
+      ({ v = Form.Sym "if-let"; _ } :: ({ v = Form.Vec [ _; _ ]; _ } as hd) :: a
+       :: ([] | [ _ ] as b)) ->
+    let simple (x : Form.t) =
+      match x.v with
+      | Form.List ({ v = Form.Sym ("return" | "set" | "break" | "continue"); _ } :: _) -> true
+      | Form.List ({ v = Form.Sym h; _ } :: _) -> not (List.mem h sugar_heads)
+      | _ -> true
+    in
+    let line = i ^ fst (expr f) in
+    if simple a && List.for_all simple b && String.length line <= width
+       && not (!inside f)
+    then Some [ line ]
+    else
+      let head = (i ^ if_let_head hd) :: slot (n + 2) a in
+      (match b with
+       | [] -> Some head
+       | [ ({ v = Form.List ({ v = Form.Sym "cond"; _ } :: args); _ } as e) ] ->
+         (match pairs args with
+          | Some (_ :: _ as prs) ->
+            let tests, else_ =
+              match List.rev prs with
+              | (k, e) :: rest when is_else k -> (List.rev rest, Some (k, e))
+              | _ -> (prs, None)
+            in
+            Some
+              (head
+               @ List.concat_map
+                   (fun ((c : Form.t), b) ->
+                      Source_text.tag c.loc.Loc.line (i ^ "elif " ^ at 1 c)
+                      :: slot (n + 2) b)
+                   tests
+               @ (match else_ with
+                  | Some ((k : Form.t), e) ->
+                    Source_text.tag k.loc.Loc.line (i ^ "else") :: slot (n + 2) e
+                  | None -> []))
+          | _ ->
+            Some (head @ [ Source_text.tag e.loc.Loc.line (i ^ "else") ] @ slot (n + 2) e))
+       | [ e ] ->
+         Some (head @ [ Source_text.tag e.loc.Loc.line (i ^ "else") ] @ slot (n + 2) e)
+       | _ -> None)
   | Form.List ({ v = Form.Sym "cond"; _ } :: args) ->
     (match pairs args with
      | None -> None
diff --git a/lib/indent_reader.ml b/lib/indent_reader.ml
index 03b13c6f..d2b68438 100644
--- a/lib/indent_reader.ml
+++ b/lib/indent_reader.ml
@@ -670,6 +670,13 @@ let no_loop loc word =
      break leaves the loop early, and continue goes on to the next round."
     word
 
+(* A [when] has one branch; an else under one is an if's. *)
+let when_else p =
+  failk "when-else" (peek p).loc
+    "a when has no else — it answers Some of its value when the test holds \
+     and None when it does not. For two branches write if c then a else b, \
+     or an if with an else block"
+
 let rec expr p : Form.t * int = binary p 1
 
 and binary p lvl : Form.t * int =
@@ -774,7 +781,7 @@ and primary p : Form.t * int =
   | NAME s ->
     let nxt = peek_at p 1 in
     let glued_lp = nxt.tok = LP && not nxt.sp in
-    if s = "if" && nxt.sp && starts_value nxt.tok then if_expr p
+    if (s = "if" || s = "when") && nxt.sp && starts_value nxt.tok then if_expr p
     else if s = "fn" && glued_lp then fn_expr p
     (* Only the Lisp loop's spellings are refused here, for a message at the
        word: [loop x = a, ...], [loop([...]):], a bare [loop] over a block
@@ -849,30 +856,76 @@ and primary p : Form.t * int =
     failk "expected-value" (where_ p) "expected a value here, and found %s"
       (show tk)
 
-(* [if c then a else b]: the one-line form, for a value. *)
+(* [if c then a else b]: the one-line form, for a value. [if let P = v then
+   a else b] and [when c then a] too. *)
 and if_expr p =
   let t = advance p in
-  let c, _ = binary p 1 in
+  let word = match t.tok with NAME w -> w | _ -> "if" in
+  let letp = if word = "if" then if_let_head p else None in
+  let c = match letp with Some m -> m | None -> fst (binary p 1) in
   (match (peek p).tok with
    | NAME "then" -> ignore (advance p)
    | _ ->
      failk "if-then" (where_ p)
-       "an if inside a line is if c then a else b, and there is no then \
-        after %s. Write the then, or start the if on its own line with its \
+       "an %s inside a line is %s, and there is no then \
+        after %s. Write the then, or start the %s on its own line with its \
         branches indented under it"
-       (text_of c));
+       word
+       (if word = "when" then "when c then a" else "if c then a else b")
+       (text_of c) word);
   let a = inline_stmt p in
   match (peek p).tok with
+  | NAME ("else" | "elif") when word = "when" -> when_else p
   | NAME "else" ->
     ignore (advance p);
     let b = inline_stmt p in
-    (mk p t.loc (Form.List [ sym t.loc "if"; c; a; b ]), 0)
+    (if_let_wrap letp (mk p t.loc (Form.List [ sym t.loc "if"; c; a; b ])), 0)
   | NAME "elif" ->
     failk "one-line-elif" (peek p).loc
       "a one-line if has then and else and no elif. Chain another if after \
        the else — if a then x else if b then y else z — or write the if over \
        several lines, where elif goes"
-  | _ -> (mk p t.loc (Form.List [ sym t.loc "when"; c; a ]), 0)
+  | _ -> (if_let_wrap letp (mk p t.loc (Form.List [ sym t.loc "when"; c; a ])), 0)
+
+(* [if let P = v]: after the [if], the pattern and the value, as the one form
+   [[P v]] that stands where the test would. [None] when no [let] follows. *)
+and if_let_head p =
+  match (peek p).tok, (peek_at p 1) with
+  | NAME "let", n when n.sp ->
+    let lt = advance p in
+    let pat, _ = unary p in
+    expect_name p "=" ~what:"= and the value the pattern is matched against";
+    let v, _ = binary p 1 in
+    Some (mk p lt.loc (Form.Vec [ pat; v ]))
+  | _ -> None
+
+(* The if an [if let] head was read into, rewritten to (if-let [P v] then
+   else): [(if [P v] a b)], [(when [P v] body ...)] and an elif chain's
+   [(cond [P v] a c2 b2 ...)], whose rest is the else. *)
+and if_let_wrap letp (f : Form.t) =
+  match letp with
+  | None -> f
+  | Some m ->
+    let il (h : Form.t) items =
+      { f with Form.v = Form.List (sym h.Form.loc "if-let" :: m :: items) }
+    in
+    let body (h : Form.t) = function
+      | [ x ] -> x
+      | (x : Form.t) :: _ as xs ->
+        Form.make (Form.List (sym x.Form.loc "do" :: xs)) x.Form.loc
+      | [] -> Form.make (Form.List [ sym h.Form.loc "do" ]) h.Form.loc
+    in
+    match f.Form.v with
+    | Form.List (({ v = Form.Sym "if"; _ } as h) :: c :: rest) when c == m -> il h rest
+    | Form.List (({ v = Form.Sym "when"; _ } as h) :: c :: b) when c == m ->
+      il h [ body h b ]
+    | Form.List (({ v = Form.Sym "cond"; _ } as h) :: c :: b1 :: rest) when c == m ->
+      (match rest with
+       | [] -> il h [ b1 ]
+       | [ { v = Form.Kw "else"; _ }; e ] -> il h [ b1; e ]
+       | (c2 : Form.t) :: _ ->
+         il h [ b1; Form.make (Form.List (sym c2.Form.loc "cond" :: rest)) c2.Form.loc ])
+    | _ -> f
 
 (* What a one-line slot takes — a match arm's value, a then or an else, the
    thing after defer: a value, or one of the statements that fit on a line,
@@ -1227,7 +1280,7 @@ let header_follow p s =
   | "fn" | "fn-" | "def" | "once" | "const" | "struct" | "union" | "data"
   | "enum" | "import" ->
     n.sp && plain_name n.tok
-  | "if" | "while" | "until" | "match" | "let" | "for" ->
+  | "if" | "when" | "while" | "until" | "match" | "let" | "for" ->
     n.sp && starts_value n.tok
     && (match n.tok with
         | NAME x when x = "=" || List.mem_assoc x assign_ops -> false
@@ -1414,7 +1467,8 @@ and value_line ?(block_ok = false) (s : st) ~after : Form.t =
     | NAME (("match" | "handler-case" | "handler-bind" | "restart-case") as w)
       when header_follow p w ->
       header s w
-    | NAME "if" when header_follow p "if" && not (then_on_line p) -> header s "if"
+    | NAME (("if" | "when") as w) when header_follow p w && not (then_on_line p) ->
+      header s w
     | _ ->
     let e, _ = expr p in
     match (peek p).tok with
@@ -1957,12 +2011,16 @@ and header (s : st) w : Form.t =
     in
     expect_eol p ~after:(text_of path);
     form [ alias; path ]
-  | "if" ->
-    let c, _ = binary p 1 in
+  | "if" | "when" ->
+    let letp = if w = "if" then if_let_head p else None in
+    let c = match letp with Some m -> m | None -> fst (binary p 1) in
     (* The elif and else clauses at the if's column, then the whole form.
        [oneline] when the if was [if c then a]: its clauses may then be
        one-line too, [elif c then x] and [else y], or take blocks. *)
     let clauses ~oneline body =
+      (match (peek p).tok with
+       | NAME ("else" | "elif") when w = "when" && not (assigns p) -> when_else p
+       | _ -> ());
       let rec elifs acc =
         match (peek p).tok with
         | NAME "elif" when not (assigns p) ->
@@ -2004,7 +2062,7 @@ and header (s : st) w : Form.t =
       in
       match els_, else_ with
       | [], None -> named "when" (c :: body)
-      | [], Some (el, e) -> form [ c; blk s l0 body; blk s el e ]
+      | [], Some (el, e) -> named "if" [ c; blk s l0 body; blk s el e ]
       | _ ->
         let pairs =
           List.concat_map (fun (c, b) -> [ c; blk s c.Form.loc b ]) ((c, body) :: els_)
@@ -2016,15 +2074,17 @@ and header (s : st) w : Form.t =
         in
         named "cond" (pairs @ tail)
     in
+    if_let_wrap letp @@
     (match (peek p).tok with
      | NAME "then" ->
        ignore (advance p);
        let a = inline_stmt p in
        (match (peek p).tok with
+        | NAME ("else" | "elif") when w = "when" -> when_else p
         | NAME "else" ->
           ignore (advance p);
           let b = inline_stmt p in
-          let f = form [ c; a; b ] in
+          let f = named "if" [ c; a; b ] in
           expect_eol p ~after:(text_of f);
           f
         | NAME "elif" ->
diff --git a/lib/load.ml b/lib/load.ml
index 3c8be027..6cd6398a 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -279,6 +279,14 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr =
                    in
                    { a with Ast.body = List.map (rename_expr owned alias bound)
                                          a.Ast.body }) arms)
+    | Ast.IfLet (sc, a, e') ->
+      let inner =
+        match a.Ast.pat with Ast.Pctor (_, ns) -> ns @ bound | _ -> bound
+      in
+      Ast.IfLet (go sc,
+                 { a with Ast.body = List.map (rename_expr owned alias inner)
+                                       a.Ast.body },
+                 Option.map go e')
     (* A quoted symbol naming something the package declares.
        [(Form.Sym {.s "Cursor"})] is what a quasiquote desugars to, and it is
        the one place a package's name survives into a *string* — which is
@@ -840,6 +848,7 @@ let rec expr_uses acc (e : Ast.expr) =
   | Ast.Call (h, args) -> go h; gos args
   | Ast.Match (sc, arms) ->
     go sc; List.iter (fun (a : Ast.arm) -> gos a.Ast.body) arms
+  | Ast.IfLet (sc, a, e') -> go sc; gos a.Ast.body; Option.iter go e'
   | Ast.Struct (n, kvs) ->
     acc := (n, e.Ast.loc) :: !acc;
     List.iter (fun (_, v) -> go v) kvs
diff --git a/lib/parse.ml b/lib/parse.ml
index 42431173..63c187ae 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -489,6 +489,18 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
 
   | Sym "cond" -> cond f args
 
+  (* (if-let [pattern value] then) and (if-let [pattern value] then else):
+     [value] is matched against [pattern], whose names are bound in [then]
+     only. Any [match] pattern may stand there. *)
+  | Sym "if-let" ->
+    (match args with
+     | { v = Vec [ p; v ]; _ } :: t :: rest when List.length rest <= 1 ->
+       let arm = { Ast.pat = pattern p; body = [ expr t ]; aloc = p.loc } in
+       mk (Ast.IfLet (expr v, arm, Option.map expr (List.nth_opt rest 0)))
+     | _ ->
+       fail f "if-let is (if-let [pattern value] then) or \
+               (if-let [pattern value] then else)")
+
   (* Short-circuiting, so they cannot be ordinary calls. *)
   | Sym "and" -> shortcircuit f args ~is_and:true
   | Sym "or" -> shortcircuit f args ~is_and:false
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index 00dced35..81b91479 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -4157,6 +4157,22 @@ flan_dyn flan_dyn_get(flan_dyn m, flan_dyn k, const uint8_t *loc,
   return flan_dyn_map_get(m, k);
 }
 
+/* The [get] builtin's, which [.field] does not share: over a map it is
+ * [flan_dyn_get], and over a vec or a text it is [at] that answers nil for an
+ * index out of range, negative included, where [at] traps. The index must
+ * still be an int — a wrong kind of key is a mistake, not an absence. */
+flan_dyn flan_dyn_get_at(flan_dyn v, flan_dyn i, const uint8_t *loc,
+                         int64_t loclen) {
+  int64_t k, len;
+  flan_obj *o;
+  if (!is_text(v) && !is_vec(v)) return flan_dyn_get(v, i, loc, loclen);
+  k = need_index(loc, loclen, "get", v, i);
+  o = dyn_obj(v);
+  len = o->kind == OBJ_VIEW ? view_len(loc, loclen, "get", o) : o->len;
+  if (k < 0 || k >= len) return flan_dyn_nil();
+  return flan_dyn_at(v, i, loc, loclen);
+}
+
 static flan_dyn contains_walk(flan_dyn m, flan_dyn k) {
   flan_obj *o = want_map(walk_loc, walk_len, walk_op, m, k);
   if (o->kind == OBJ_VIEW) {
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
index 01a29f12..5bffe658 100644
--- a/runtime/flan_dyn.h
+++ b/runtime/flan_dyn.h
@@ -245,6 +245,10 @@ flan_dyn flan_dyn_map_get(flan_dyn m, flan_dyn k);
 /* [get]'s, and a dyn's [.field]: [flan_dyn_map_get] with a site. */
 flan_dyn flan_dyn_get(flan_dyn m, flan_dyn k, const uint8_t *loc,
                       int64_t loclen);
+/* The [get] builtin's: [flan_dyn_get] over a map, and over a vec or a text
+ * the element, or nil for an index out of range. */
+flan_dyn flan_dyn_get_at(flan_dyn v, flan_dyn i, const uint8_t *loc,
+                         int64_t loclen);
 void     flan_dyn_map_set(flan_dyn m, flan_dyn k, flan_dyn v);
 /* [put]'s: [flan_dyn_map_set], with the site a typed class slot's refusal
  * prints. */
diff --git a/spec-syntax.md b/spec-syntax.md
index e7e4cfc6..df8a70ca 100644
--- a/spec-syntax.md
+++ b/spec-syntax.md
@@ -214,6 +214,16 @@ Each item: the proposal, then the reason in one line.
   line after a one-line `if c then a`, at its column, continues it (section
   3, item 6); each such clause is one-line (`elif c then x`, `else y`) or
   takes a block.
+- **`when c`** plus a block, or `when c then a`, reads as `when`, which is
+  what an `if` without `else` reads as too. No `else` or `elif` follows it.
+  A `when` whose value is kept (a `let`'s value, an argument, a return) gives
+  `Some(a)` when `c` holds and `None` when it does not; where a `dyn` is
+  wanted, `a` or `nil`. As a statement it gives nothing. **Built.**
+- **`if let P = v`** plus a block reads as `(if-let [P v] then)`; `elif` and
+  `else` follow as for `if`, the rest of the chain being the `if-let`'s else.
+  `P` is any `match` pattern, and its names are bound in the block only. One
+  line: `if let Some(g) = o then g else 0`. A pattern that cannot fail, a
+  plain name or `_`, is refused toward `let`. **Built.**
 - **`while c`, `until c`**, optional label first: `while :outer c`. **Built.**
 - **`for i in range(n)`**, `range(a, b)`, `range(a, b, step)` read as
   `dotimes`. `range` here is syntax, not a function. `..` is avoided because
diff --git a/test/programs/get-checked.flan b/test/programs/get-checked.flan
new file mode 100644
index 00000000..c060cc12
--- /dev/null
+++ b/test/programs/get-checked.flan
@@ -0,0 +1,63 @@
+;;;; get over an array, a slice, a string and a Vec is at that answers None
+;;;; for an index out of range, negative included, one index per dimension.
+;;;; Over a dyn it answers nil, and more keys walk a level each.
+
+(defn show [o (Option i32)] ()
+  (match o (Some v) (println v) None (println "none")))
+
+(defn three [] (Vec i32)
+  (let [v (vec-new i32)] (push v 10) (push v 20) (push v 30) v))
+
+(defn dvec [] dyn [10 [20 21] 30])
+(defn dmap [] dyn {:a 1 :b [5 6]})
+
+(defn main [] ()
+  (let [a [1 2 3]
+        grid [[1 2 3] [4 5 6]]
+        s (slice a)
+        v (three)
+        n (length a)
+        vv (vec-new (Vec i32) context/temp)]
+    (push vv v)
+    ;; -1, 0, len-1 and len on an array.
+    (show (get a -1))
+    (show (get a 0))
+    (show (get a (- n 1)))
+    (show (get a n))
+    ;; Two dimensions, each tested.
+    (let [r 0 c 1]
+      (show (get grid (+ r 1) (- c 1)))
+      (show (get grid (- r 1) c))
+      (show (get grid r (+ c 2))))
+    (show (get grid 1 2))
+    (show (get grid 2 0))
+    ;; A slice.
+    (show (get s 2))
+    (show (get s 3))
+    ;; A Vec, and one a call answered.
+    (show (get v -1))
+    (show (get v 0))
+    (show (get v 2))
+    (show (get v 3))
+    (show (get (three) 1))
+    ;; A Vec of Vecs: the inner length is tested only once the outer index is.
+    (show (get vv 0 2))
+    (show (get vv 0 3))
+    (show (get vv 1 0))
+    ;; A string's byte.
+    (match (get "hey" 1) (Some b) (println b) None (println "none"))
+    (match (get "hey" 3) (Some b) (println b) None (println "none")))
+  ;; Dyn.
+  (let [d (dvec) m (dmap)]
+    (println (get d -1))
+    (println (get d 0))
+    (println (get d 2))
+    (println (get d 3))
+    (println (get d 1 1))
+    (println (get d 1 2))
+    (println (get d 5 0))
+    (println (get m :a))
+    (println (get m :z))
+    (println (get m :b 1))
+    (println (get m :z 1))
+    (println (.a m))))
diff --git a/test/programs/if-let.fln b/test/programs/if-let.fln
new file mode 100644
index 00000000..79412fc1
--- /dev/null
+++ b/test/programs/if-let.fln
@@ -0,0 +1,56 @@
+;; if let: the block runs when the pattern matches, its names bound there only.
+
+data Shape
+  Rect(w: i32, h: i32)
+  Dot
+
+enum Dir
+  north = 0
+  south = 1
+
+fn describe(o: Option(i32), k: i32) -> i32
+  if let Some(g) = o
+    g + 1
+  elif k > 5
+    100
+  else
+    0
+
+fn first(xs: [3 i32]) -> i32
+  if let Some(x) = get(xs, 0) then x else -1
+
+;; Nested: a pattern tested inside the block of another.
+fn area(s: Option(Shape)) -> i32
+  if let Some(x) = s
+    if let Rect(w, h) = x
+      w * h
+    else
+      -1
+  else
+    -2
+
+fn main()
+  let g = 7
+  println(describe(Some(4), 0))
+  println(describe(None, 9))
+  println(describe(None, 1))
+  println(first([9, 8, 7]))
+  ;; Shadowing: g is the payload inside the block and the outer g after it.
+  if let Some(g) = Some(1)
+    println(g)
+  println(g)
+  ;; Any match pattern.
+  if let None = get([1, 2], 5)
+    println("absent")
+  if let :north = Dir.north
+    println("north")
+  println(area(Some(Shape.Rect{.w 2 .h 3})))
+  println(area(Some(Shape.Dot)))
+  println(area(None))
+  ;; when on one line and with a block.
+  let w = when g > 3 then g * 2
+  match w
+    Some(v) -> println(v)
+    None -> println("none")
+  when g > 1
+    println("when block")
diff --git a/test/programs/when-value.flan b/test/programs/when-value.flan
new file mode 100644
index 00000000..5b4f9a9f
--- /dev/null
+++ b/test/programs/when-value.flan
@@ -0,0 +1,42 @@
+;;;; A when whose value is kept answers an Option: Some of its body when the
+;;;; test holds, None when it does not. As a statement it answers nothing.
+;;;; Where a dyn is wanted it answers the body or nil, since dyn has no
+;;;; Option. A body that is already an Option is not flattened.
+
+(defn show [o (Option i32)] ()
+  (match o (Some v) (println v) None (println "none")))
+
+;; Returned: the return type is the want.
+(defn half [n i32] (Option i32) (when (= 0 (% n 2)) (/ n 2)))
+
+;; Nested, as Rust's bool::then: None from the body stays apart from a
+;; failed test.
+(defn wrap [c bool o (Option i32)] (Option (Option i32)) (when c o))
+
+(defn level [oo (Option (Option i32))] ()
+  (match oo
+    (Some o) (match o (Some v) (println v) None (println "some none"))
+    None (println "none")))
+
+;; Dyn: the body or nil.
+(defn dyn-when [x] dyn (when x 5))
+
+(defn main [] ()
+  (show (half 10))
+  (show (half 7))
+  ;; A let's value.
+  (let [a (when (> 3 2) 42)
+        b (when (> 2 3) 42)]
+    (show a)
+    (show b))
+  ;; An argument.
+  (show (when true 9))
+  (level (wrap true (Some 1)))
+  (level (wrap true None))
+  (level (wrap false (Some 1)))
+  (println (dyn-when true))
+  (println (dyn-when nil))
+  ;; Statements, unchanged.
+  (when true (println "ran"))
+  (when false (println "not run"))
+  (println "end"))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index bb0d75f7..1789987c 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2058,6 +2058,29 @@ let () =
       dyn_if_truthy_out;
     outputs ~x86:true "dyn if truthiness, --x86" "programs/dyn-if-truthy.flan"
       dyn_if_truthy_out;
+    (* A kept when is an Option; get is a checked lookup; if let. *)
+    let when_value_out =
+      "5\nnone\n42\nnone\n9\n1\nsome none\nnone\n5\nnil\nran\nend\n"
+    in
+    outputs "when as a value" "programs/when-value.flan" when_value_out;
+    outputs ~opt:"-O0" "when as a value, -O0" "programs/when-value.flan" when_value_out;
+    outputs ~x86:true "when as a value, --x86" "programs/when-value.flan" when_value_out;
+    let get_checked_out =
+      "none\n1\n3\nnone\n4\nnone\nnone\n6\nnone\n3\nnone\n\
+       none\n10\n30\nnone\n20\n30\nnone\nnone\n101\nnone\n\
+       nil\n10\n30\nnil\n21\nnil\nnil\n1\nnil\n6\nnil\n1\n"
+    in
+    outputs "get as a checked lookup" "programs/get-checked.flan" get_checked_out;
+    outputs ~opt:"-O0" "get as a checked lookup, -O0" "programs/get-checked.flan"
+      get_checked_out;
+    outputs ~x86:true "get as a checked lookup, --x86" "programs/get-checked.flan"
+      get_checked_out;
+    let if_let_out =
+      "5\n100\n0\n9\n1\n7\nabsent\nnorth\n6\n-1\n-2\n14\nwhen block\n"
+    in
+    outputs "if let" "programs/if-let.fln" if_let_out;
+    outputs ~opt:"-O0" "if let, -O0" "programs/if-let.fln" if_let_out;
+    outputs ~x86:true "if let, --x86" "programs/if-let.fln" if_let_out;
     (* format-f64, the first number formatter a caller can steer. The three
        lines that would ship wrong are pinned deliberately: 0.999995 at five
        places, where the rounded fraction equals the scale and is the next
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 6b853e5f..d0e4ede2 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -8125,5 +8125,23 @@ let () =
   parse_rejects "_ in a defgeneric's return slot"
     ~needle:"defgeneric's methods each have their own"
     "(defgeneric area [s] _)";
+  (* if-let refuses a pattern that cannot fail, toward let; the program half
+     is programs/if-let.flan. *)
+  rejects_check "if-let over a plain name"
+    ~needle:"the pattern g is a plain name, which always matches"
+    "(defn main [] () (if-let [g (Some 1)] (println g)))";
+  rejects_check "and says let" ~needle:"(let [g ...] ...)"
+    "(defn main [] () (if-let [g (Some 1)] (println g)))";
+  rejects_check "if-let over _" ~needle:"the pattern _ always matches"
+    "(defn main [] () (if-let [_ (Some 1)] (println 1)))";
+  accepts "if-let over a case with no fields"
+    "(defdata S [(A []) (B [])])\n(defn main [] () (if-let [A S.B] (println 1)))";
+  (* A used when is an Option, and a statement's is nothing. *)
+  accepts "a let's when is an Option"
+    "(defn main [] () (let [x (the (Option i32) (when true 1))] (println x)))";
+  rejects_check "a when is not its branch's type" ~needle:"(Option i32)"
+    "(defn f [] i32 (when true 1))\n(defn main [] ())";
+  rejects_check "a map's get takes one key" ~needle:"a map's get takes one key"
+    "(defn main [] () (let [m (map-new i32 i32)] (println (get m 1 2))))";
 
   Test_support.report ()
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index fc970edb..37a99d9f 100644
--- a/test/test_syntax.ml
+++ b/test/test_syntax.ml
@@ -933,6 +933,26 @@ let () =
     "  sort-by(xs, fn(a, b) =>\n    g(a)\n    a < b)";
   round "one closer for a call in a call"
     "(defn f [] () (println (run (fn [] (g) 1))))" "  println(run(fn() =>\n    g()\n    1))";
+  (* if let and when, read both ways and printed back. *)
+  round "if let with a block and an else"
+    "(defn f [o (Option i32)] i32 (if-let [(Some g) o] (do (println g) g) 0))"
+    "  if let Some(g) = o\n    println(g)\n    g\n  else\n    0";
+  round "if let on one line"
+    "(defn f [o (Option i32)] i32 (if-let [(Some g) o] g 0))"
+    "  if let Some(g) = o then g else 0";
+  round "if let with elif"
+    "(defn f [o (Option i32) k i32] i32 (if-let [(Some g) o] (+ g 1) (cond (> k 5) 100 :else 0)))"
+    "  elif k > 5\n    100\n  else\n    0";
+  round "if let with no else" "(defn f [o (Option i32)] () (if-let [(Some g) o] (do (println g) (println g))))"
+    "  if let Some(g) = o\n    println(g)";
+  round "a kept when" "(defn f [] () (let [w (when (> a 1) 2)] (g w)))"
+    "  let w = when a > 1 then 2";
+  reads "when with a block" "when a\n  b()\n  c()" "(when a (b) (c))";
+  reads "when on one line" "when a then b()" "(when a (b))";
+  reads "if let with elif and no else" "if let None = o\n  a()\nelif c\n  b()"
+    "(if-let [None o] (a) (cond c (b)))";
+  refuses "when has no else" "when a then b() else c()" "indent/when-else" "a when has no else";
+  refuses "nor an else block" "when a\n  b()\nelse\n  c()" "indent/when-else" "a when has no else";
   round "a typed block lambda in a call"
     "(defn f [] () (h (the (Fn [C] bool) (fn [c] (g c) (> (.n c) 3)))))"
     "  h(fn(c: C) -> bool =>\n    g(c)\n    c.n > 3)";