Definitions with lexical variables
The following example demonstrates lexical variable bindings in word definitions. The quadratic-roots word is defined with ::, so it takes its inputs from the top three elements of the datastack and binds them to the variables a, b, and c. In the body, the disc variable is bound using :> and then used in the following line of code.
USING: locals math math.functions kernel ; IN: scratchpad :: quadratic-roots ( a b c -- x y ) b sq 4 a c * * - sqrt :> disc b neg disc [ + ] [ - ] 2bi [ 2 a * / ] bi@ ; 1.0 1.0 -6.0 quadratic-roots
--- Data stack: 2.0 -3.0

If you wanted to perform the quadratic formula interactively from the listener, you could use [let to provide a scope for the variables:
USING: locals math math.functions kernel ; IN: scratchpad [let 1.0 :> a 1.0 :> b -6.0 :> c b sq 4 a c * * - sqrt :> disc b neg disc [ + ] [ - ] 2bi [ 2 a * / ] bi@ ]
--- Data stack: 2.0 -3.0

Quotations with lexical variables, and closures
These next two examples demonstrate lexical variable bindings in quotations defined with [|. In this example, the values 5 and 3 are put on the datastack. When the quotation is called, it takes those values as inputs and binds them respectively to m and n before executing the quotation:
USING: kernel locals math ; IN: scratchpad 5 3 [| m n | m n - ] call( x x -- x )
--- Data stack: 2

In this example, the adder word creates a quotation that closes over its argument n. When called, the result quotation of 5 adder pulls 3 off the datastack and binds it to m, which is added to the value 5 bound to n in the outer scope of adder:
USING: kernel locals math ; IN: scratchpad :: adder ( n -- quot ) [| m | m n + ] ; 3 5 adder call( x -- x )
--- Data stack: 8

Mutable bindings
This next example demonstrates closures and mutable variable bindings. The <counter> word outputs a tuple containing a pair of quotations that respectively increment and decrement an internal counter in the mutable value variable and then return the new value. The quotations close over the counter, so each invocation of the word gives new quotations with a new internal counter.
USING: accessors locals kernel math ; IN: scratchpad TUPLE: counter adder subtractor ; :: <counter> ( -- counter ) 0 :> value! counter new [ value 1 + dup value! ] >>adder [ value 1 - dup value! ] >>subtractor ; <counter> [ adder>> call( -- x ) ] [ adder>> call( -- x ) ] [ subtractor>> call( -- x ) ] tri
--- Data stack: 1 2 1

The same variable name can be bound multiple times in the same scope. This is different from reassigning the value of a mutable variable. The most recent binding for a variable name will mask previous bindings for that name. However, the old binding referring to the previous value can still persist in closures. The following contrived example demonstrates this:
USING: kernel locals ; IN: scratchpad :: rebinding-example ( -- quot1 quot2 ) 5 :> a [ a ] 6 :> a [ a ] ; :: mutable-example ( -- quot1 quot2 ) 5 :> a! [ a ] 6 a! [ a ] ; rebinding-example [ call( -- x ) ] bi@ mutable-example [ call( -- x ) ] bi@
--- Data stack: 5 6 6 6

In rebinding-example, the binding of a to 5 is closed over in the first quotation, and the binding of a to 6 is closed over in the second, so calling both quotations results in 5 and 6 respectively. By contrast, in mutable-example, both quotations close over a single binding of a. Even though a is assigned to 6 after the first quotation is made, calling either quotation will output the new value of a.

Lexical variables in literals
Some kinds of literals can include references to lexical variables as described in Lexical variables in literals. For example, the 3array word could be implemented as follows:
USING: locals ; IN: scratchpad :: my-3array ( x y z -- array ) { x y z } ; 1 "two" 3.0 my-3array
--- Data stack: { 1 "two" 3.0 }