diff --git a/TODO.org b/TODO.org
index 3639d240..780fcf65 100644
--- a/TODO.org
+++ b/TODO.org
@@ -26,14 +26,13 @@ and any storage; a dev build checks a view against its frame or allocation and t
 when stale, a release build does not. Waits on the dyn-unless-annotated design.
 
 ** NEXT Dyn unless annotated
-Decided 2026-09-25: in both syntaxes an unannotated value is dyn — [6 2 4 9] is a dyn
-vector, 1 a dyn integer — and a typed value needs an annotation. Decided 2026-09-26:
-the plain rule — a literal is dyn wherever nothing wants a type, typed functions
-included; a value from a typed source keeps its type; for/dotimes counters stay i32; a
-warning marks a dyn let meeting typed code in a typed function. Migration in the
-design's order: str rename, views of any type, dyn-meets-typed fixes, literals built
-once, the switch with the warning, annotation script, flip, String.
-
+Decided 2026-09-26, replacing the plain rule: number, bool and char literals are typed,
+their type inferred from their uses inside the function (never across functions); an
+unconstrained integer literal is int (i32) and a float literal float (f32); uses that
+disagree are refused with a request for an annotation. Vector, map and text literals
+are dyn unless something typed wants them. A typed value is boxed where it goes into
+dyn, and a dyn unboxed (checked) where typed code needs it; typed beside dyn in an
+operator gives dyn. Dyn integers stay i64 and dyn floats f64.
 ** DONE Dynamic-first, and the dyn half of the language
 CLOSED: [2026-09-20]
 An unannotated parameter or return is =dyn=: a NaN-boxed value over a mark-sweep
@@ -650,6 +649,11 @@ Decided 2026-09-26: a lambda's body follows ~=>~, and ~=>~ is its only spelling
 takes an indented block even inside brackets, closing where the brackets close:
 ~sort-by(xs, fn(a, b) =>~ plus a block.
 
+** NEXT A let takes several bindings on indented lines
+Decided 2026-09-26: lines indented under a ~let~ that are ~name = v~ or ~name: T = v~ are
+more bindings of the same let; anything else there stays refused. flan convert writes
+consecutive lets this way.
+
 ** TODO Hard-coded code in messages is still paren syntax in a .fln file
 Types follow the code's syntax now (=Types.spell=). Hints written into a message's
 text — =(Ptr %s)=, =(clone v)=, =(the T x)= in most of =check.ml= and =parse.ml=, the