docs: add variables; rework scope (#11062)

Co-authored-by: Valentin Gagarin <valentin@gagarin.work>

doc/manual/src/SUMMARY.md.in

@@ -28,6 +28,7 @@
   - [Data Types](language/types.md)
     - [String context](language/string-context.md)
   - [Syntax and semantics](language/syntax.md)
+    - [Variables](language/variables.md)
     - [Identifiers](language/identifiers.md)
     - [Scoping rules](language/scope.md)
     - [String interpolation](language/string-interpolation.md)

doc/manual/src/language/identifiers.md

@@ -22,7 +22,7 @@ A name can be an [identifier](#identifier) or a [string literal](./syntax.md#str
 >
 > *name* → *identifier* | *string*
 
-Names are used in [attribute sets](./syntax.md#attrs-literal), [`let` bindings](./syntax.md#let-expressions), and [`inherit`](./syntax.md#inheriting attributes).
+Names are used in [attribute sets](./syntax.md#attrs-literal), [`let` bindings](./syntax.md#let-expressions), and [`inherit`](./syntax.md#inheriting-attributes).
 
 # Keywords
 

doc/manual/src/language/scope.md

@@ -1,14 +1,28 @@
 # Scoping rules
 
-Nix is [statically scoped](https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexical_scope), but with multiple scopes and shadowing rules.
+A *scope* in the Nix language is a dictionary keyed by [name](./identifiers.md#names), mapping each name to an expression and a *definition type*.
+The definition type is either *explicit* or *implicit*.
+Each entry in this dictionary is a *definition*.
 
-* primary scope: explicitly-bound variables
+Explicit definitions are created by the following expressions:
-  * [`let`](./syntax.md#let-expressions)
+- [let-expressions](syntax.md#let-expressions)
-  * [`inherit`](./syntax.md#inheriting-attributes)
+- [recursive attribute set literals](syntax.md#recursive-sets) (`rec`)
-  * [function](./syntax.md#functions) arguments
+- [function literals](syntax.md#functions)
 
-* secondary scope: implicitly-bound variables
+Implicit definitions are only created by [with-expressions](./syntax.md#with-expressions).
-  * [`with`](./syntax.md#with-expressions)
 
-Primary scope takes precedence over secondary scope.
+Every expression is *enclosed* by a scope.
-See [`with`](./syntax.md#with-expressions) for a detailed example.
+The outermost expression is enclosed by the [built-in, global scope](./builtins.md), which contains only explicit definitions.
+The respective definition types *extend* their enclosing scope by adding new definitions, or replacing existing ones with the same name.
+An explicit definition can replace a definition of any type; an implicit definition can only replace another implicit definition.
+
+Each of the above expressions defines which of its subexpressions are enclosed by the extended scope.
+In all other cases, the same scope that encloses an expression is the enclosing scope for its subexpressions.
+
+The Nix language is [statically scoped](https://en.wikipedia.org/wiki/Scope_(computer_science)#Lexical_scope);
+the value of a variable is determined only by the variable's enclosing scope, and not by the dynamic context in which the variable is evaluated.
+
+> **Note**
+>
+> Expressions entered into the [Nix REPL](@docroot@/command-ref/new-cli/nix3-repl.md) are enclosed by a scope that can be extended by command line arguments or previous REPL commands.
+> These ways of extending scope are not, strictly speaking, part of the Nix language.

doc/manual/src/language/variables.md

@@ -0,0 +1,10 @@
+# Variables
+
+A *variable* is an [identifier](identifiers.md) used as an expression.
+
+> **Syntax**
+>
+> *expression* → *identifier*
+
+A variable must have the same name as a definition in the [scope](./scope.md) that encloses it.
+The value of a variable is the value of the corresponding expression in the enclosing scope.