diff --git a/scrbl/let-assert.scrbl b/scrbl/let-assert.scrbl
index 3971c29..b571d4b 100644
--- a/scrbl/let-assert.scrbl
+++ b/scrbl/let-assert.scrbl
@@ -4,255 +4,209 @@
                      "../main.rkt"))
 
 @title{let/assert}
-
 @author[@author+email["Hans Dijkema" "hans@dijkewijk.nl"]]
 
 @defmodule[let-assert]
 
-This module provides @racket[let/assert], a small sequential binding
-form for defensive programming. It is especially useful around FFI calls,
-where failure is often reported by ordinary values: @racket[#f] for a
-null pointer, a negative integer for an error code, or a non-zero integer
-for a failed C-style status result.
+This module provides @racket[let/assert], a small sequential binding form
+with local assertions.  It is useful for defensive programming around FFI
+bindings: checks for null pointers, exit codes, and similar failure values can
+be kept close to the binding that produced them, while the body stays on the
+happy path.  When an assertion fails, the whole @racket[let/assert] expression
+returns the associated fallback value.
 
-The form is implemented with @racket[call/cc]. A failed assertion does
-not raise an exception. Instead, it invokes an internal escape
-continuation and returns the supplied failure value as the result of the
-whole @racket[let/assert] expression.
+@section{Binding with assertions}
 
 @defform[
-(let/assert
-  ((id expr)
-   (id expr assert-expr failure-expr)
-   ...)
-  body ...)
-]{
+(let/assert (binding ...) body ...+)
+#:grammar
+([binding [id expr]
+          [id expr predicate-expr fallback-expr]])]{
 
-Evaluates the bindings from left to right, using @racket[let*]
-semantics. Later bindings may refer to earlier ones.
+Evaluates the bindings from left to right and then evaluates the body.  Later
+bindings may refer to earlier bindings, as with @racket[let*].
+
+The implementation expands through an internal helper into nested
+@racket[let] and @racket[cond] forms.  There is no exception-based control
+flow in this version: a failing assertion directly selects the fallback result
+for that binding.
+
+A binding of the form @racket[[id expr]] simply binds @racket[id] to
+@racket[expr].
 
 A binding of the form
+@racket[[id expr predicate-expr fallback-expr]] evaluates @racket[expr] once,
+binds the result to @racket[id], and then calls @racket[predicate-expr] with
+that value.  If the predicate returns a true value, evaluation continues with
+the next binding or with the body.  If the predicate returns @racket[#f], the
+body is not evaluated and the complete @racket[let/assert] form returns
+@racket[fallback-expr].
 
-@racketblock[
-(id expr)
-]
-
-is a plain sequential binding.
-
-A binding of the form
-
-@racketblock[
-(id expr assert-expr failure-expr)
-]
-
-evaluates @racket[expr] once and applies @racket[assert-expr] to the
-result. If the assertion succeeds, @racket[id] is bound to the original
-value. If the assertion fails, @racket[failure-expr] is returned as the
-result of the whole @racket[let/assert] form.
-
-The escape continuation is internal. It is not part of the surface syntax
-and is not visible in the body.
-
-@racketblock[
-(define (half-positive n)
-  (let/assert
-    ((x n a->0? 'not-positive))
-    (/ x 2)))
-]
-
-The result is @racket[5] for @racket[(half-positive 10)] and
-@racket['not-positive] for @racket[(half-positive 0)].
-
-Because @racket[let/assert] uses @racket[call/cc], failure is local
-control flow. There is no exception object, no exception handler, and no
-dynamic catching of unrelated failures.
+The fallback expression belongs to the binding where the assertion is made.
+This keeps failure handling close to the operation that may fail.
 }
 
-@section{Assertion constructors}
+@racketblock[
+(let/assert ([x 10 (a->? 0) 'too-small]
+             [y (+ x 2) (a-=? 12) 'wrong-value])
+  y)
+]
+
+This expression returns @racket[12].  The second binding may use @racket[x],
+because the bindings are evaluated sequentially.
+
+@racketblock[
+(let/assert ([ptr (open-native-handle) a-!nullptr? 'open-failed]
+             [ret (use-native-handle ptr) (a->=? 0) 'call-failed])
+  'ok)
+]
+
+This style is useful around FFI code.  If @racket[open-native-handle] returns
+@racket[#f], the result is @racket['open-failed].  If
+@racket[use-native-handle] returns a negative status code, the result is
+@racket['call-failed].  Otherwise the body is evaluated and the result is
+@racket['ok].
+
+@section{FFI-style example}
+
+Many C libraries, including FFmpeg-style APIs, report failure through null
+pointers or integer return codes.  A typical wrapper can therefore keep the
+normal path small:
+
+@racketblock[
+(define (open-decoder file)
+  (let/assert ([ctx (avformat-open-input file)
+                    a-!nullptr?
+                    'open-input-failed]
+               [ret (avformat-find-stream-info ctx)
+                    (a->=? 0)
+                    'stream-info-failed]
+               [stream (find-best-audio-stream ctx)
+                       a-!nullptr?
+                       'no-audio-stream])
+    stream))
+]
+
+The example is intentionally written as wrapper-style Racket code rather than
+as a direct FFmpeg binding.  The important point is the shape: pointer-returning
+operations are checked with @racket[a-!nullptr?], while return-code operations
+are checked with predicates such as @racket[(a->=? 0)].
+
+@section{Creating assertion factories}
 
 @defform[(make-assert name not-name pred)]{
 
-Defines two assertion-constructor forms.
+Defines two assertion factories.
 
-The generated @racket[name] form creates a predicate that compares its
-argument with a constant using @racket[pred]:
+The form @racket[(name constant)] produces a unary predicate that applies
+@racket[pred] to the checked value and @racket[constant]:
 
 @racketblock[
-((name const) value)
+(lambda (x) (pred x constant))
 ]
 
-is equivalent to:
+The form @racket[(not-name constant)] produces the negated variant:
 
 @racketblock[
-(λ (x) (pred x const))
+(lambda (x) (not (pred x constant)))
 ]
 
-The generated @racket[not-name] form creates the negated predicate:
+For example:
 
 @racketblock[
-(λ (x) (not (pred x const)))
+(make-assert a-eq? a-!eq? eq?)
 ]
 
-For example, the module defines:
-
-@racketblock[
-(make-assert a-eq?  a-!eq?  eq?)
-(make-assert a->?   a-<=?   >)
-(make-assert a->=?  a-<?    >=)
-(make-assert a-=?   a-!=?   =)
-]
-
-The negated forms are logical negations of the positive predicate.
+defines @racket[a-eq?] and @racket[a-!eq?].
 }
 
-@defform[(a-eq? const)]{
-Creates a predicate that accepts values @racket[eq?] to @racket[const].
+@section{Assertion factories}
+
+@defform[(a-eq? constant)]{
+Produces a predicate that accepts values for which
+@racket[(eq? value constant)] is true.
 }
 
-@defform[(a-!eq? const)]{
-Creates a predicate that accepts values not @racket[eq?] to
-@racket[const].
+@defform[(a-!eq? constant)]{
+Produces a predicate that accepts values for which
+@racket[(eq? value constant)] is false.
 }
 
-@defform[(a->? const)]{
-Creates a predicate that accepts values greater than @racket[const].
+@defform[(a->? constant)]{
+Produces a predicate that accepts values greater than @racket[constant].
 }
 
-@defform[(a-<=? const)]{
-Creates the negation of @racket[(a->? const)].
+@defform[(a-<=? constant)]{
+Produces a predicate that accepts values for which @racket[(> value constant)]
+is false.
 }
 
-@defform[(a->=? const)]{
-Creates a predicate that accepts values greater than or equal to
-@racket[const].
+@defform[(a->=? constant)]{
+Produces a predicate that accepts values greater than or equal to
+@racket[constant].
 }
 
-@defform[(a-<? const)]{
-Creates the negation of @racket[(a->=? const)].
+@defform[(a-<? constant)]{
+Produces a predicate that accepts values for which
+@racket[(>= value constant)] is false.
 }
 
-@defform[(a-=? const)]{
-Creates a predicate that accepts values numerically equal to
-@racket[const].
+@defform[(a-=? constant)]{
+Produces a predicate that accepts values numerically equal to
+@racket[constant].
 }
 
-@defform[(a-!=? const)]{
-Creates the negation of @racket[(a-=? const)].
+@defform[(a-!=? constant)]{
+Produces a predicate that accepts values not numerically equal to
+@racket[constant].
 }
 
-@section{Built-in predicates}
+The negated factories are exact negations of their corresponding predicate.
+For ordinary numeric values, @racket[(a-<=? n)] behaves like a less-than-or-equal
+check and @racket[(a-<? n)] behaves like a less-than check, but they are
+implemented as negations of @racket[>] and @racket[>=].
+
+@section{Ready-made predicates}
 
 @defproc[(a-=0? [x number?]) boolean?]{
-Accepts values numerically equal to zero.
+Returns @racket[#t] when @racket[x] is numerically equal to zero.
 }
 
 @defproc[(a-!=0? [x number?]) boolean?]{
-Accepts values not numerically equal to zero.
+Returns @racket[#t] when @racket[x] is not numerically equal to zero.
 }
 
 @defproc[(a->0? [x real?]) boolean?]{
-Accepts values greater than zero.
+Returns @racket[#t] when @racket[x] is greater than zero.
 }
 
 @defproc[(a->=0? [x real?]) boolean?]{
-Accepts values greater than or equal to zero.
+Returns @racket[#t] when @racket[x] is greater than or equal to zero.
 }
 
 @defproc[(a-<0? [x real?]) boolean?]{
-Accepts values less than zero.
+Returns @racket[#t] when @racket[x] is less than zero.
 }
 
 @defproc[(a-<=0? [x real?]) boolean?]{
-Accepts values less than or equal to zero.
+Returns @racket[#t] when @racket[x] is less than or equal to zero.
 }
 
-@defthing[a-true? procedure?]{
-A predicate that accepts only @racket[#t].
+@defproc[(a-true? [x any/c]) boolean?]{
+Returns @racket[#t] when @racket[x] is @racket[eq?] to @racket[#t].
 }
 
-@defthing[a-false? procedure?]{
-A predicate that accepts only @racket[#f].
+@defproc[(a-false? [x any/c]) boolean?]{
+Returns @racket[#t] when @racket[x] is @racket[eq?] to @racket[#f].
 }
 
-@defthing[a-nullptr? procedure?]{
-A predicate that accepts @racket[#f]. This is intended for FFI bindings
-where a native null pointer is represented as @racket[#f].
+@defproc[(a-nullptr? [x any/c]) boolean?]{
+Returns @racket[#t] when @racket[x] is @racket[eq?] to @racket[#f].  The name
+is intended for FFI code where @racket[#f] represents a null pointer.
 }
 
-@defthing[a-!nullptr? procedure?]{
-A predicate that accepts values that are not @racket[#f]. This is useful
-for checking successful pointer allocation in FFI code.
-}
-
-@section{Examples}
-
-A simple status-code check:
-
-@racketblock[
-(define (open-status r)
-  (let/assert
-    ((status r a-=0? 'open-failed))
-    'opened))
-]
-
-Here @racket[(open-status 0)] returns @racket['opened], while
-@racket[(open-status -1)] returns @racket['open-failed].
-
-A pointer-style check:
-
-@racketblock[
-(define (use-context maybe-ctx)
-  (let/assert
-    ((ctx maybe-ctx a-!nullptr? 'no-context))
-    ctx))
-]
-
-Here @racket[#f] is treated as a failed native pointer result.
-
-Plain bindings and asserted bindings may be mixed. Since the form uses
-@racket[let*] semantics, later expressions can refer to earlier values:
-
-@racketblock[
-(define (make-scaled-size width height scale)
-  (let/assert
-    ((w width  a->0? 'bad-width)
-     (h height a->0? 'bad-height)
-     (s scale  a->0? 'bad-scale)
-     (area (* w h)))
-    (* area s)))
-]
-
-The expression @racket[area] is only evaluated after @racket[w] and
-@racket[h] have passed their assertions.
-
-@subsection{FFmpeg-style null pointers}
-
-Many FFmpeg functions return a native pointer, where @racket[#f]
-represents a null pointer. Since @racket[let/assert] uses sequential
-@racket[let*] semantics, later bindings may depend on earlier checked
-pointer results.
-
-@racketblock[
-(define (make-stream-codec-context stream)
-  (let/assert
-    ((codecpar (AVStream-codecpar stream) a-!nullptr?
-               'missing-codec-parameters)
-
-     (codec    (avcodec-find-decoder
-                (AVCodecParameters-codec-id codecpar))
-               a-!nullptr?
-               'decoder-not-found)
-
-     (ctx      (avcodec-alloc-context3 codec) a-!nullptr?
-               'alloc-codec-context-failed))
-    ctx))
-]
-
-If @racket[avcodec-find-decoder] returns @racket[#f], the whole
-@racket[let/assert] expression returns @racket['decoder-not-found].
-The second binding is then not evaluated.
-
-If @racket[codec] is a valid pointer, it is used by the next binding.
-If @racket[avcodec-alloc-context3] returns @racket[#f], the expression
-returns @racket['alloc-codec-context-failed]. Otherwise @racket[ctx] is
-bound to the allocated context and returned by the body.
\ No newline at end of file
+@defproc[(a-!nullptr? [x any/c]) boolean?]{
+Returns @racket[#t] when @racket[x] is not @racket[eq?] to @racket[#f].  This
+is often the success predicate for FFI calls that return either a native
+pointer or @racket[#f].
+}
\ No newline at end of file