address review comments

Author: zliu41

src/plutus/builtin.md

@@ -1 +1 @@
-# Builtin Types and Functions
+# Built-in Types and Functions

src/plutus/syntax.md

@@ -1,31 +1,33 @@
 # Syntax
 
-The following listing shows the syntax of Plutus.
+The following listing shows the concrete syntax of Plutus.
 The corresponding Haskell definition can be found in [UntypedPlutusCore.Core.Type](https://plutus.cardano.intersectmbo.org/haddock/latest/plutus-core/UntypedPlutusCore-Core-Type.html#t:Term).
 
 ```text
 𝐿, 𝑀, 𝑁 ∈ Term ::= 𝑥              variable
                   | (con T 𝑐)      constant 𝑐 with type T
-                  | (builtin 𝑏)    builtin
+                  | (builtin 𝑏)    built-in
                   | (lam 𝑥 𝑀)     lambda abstraction
                   | [𝑀 𝑁]         application
                   | (delay 𝑀)     delayed execution of a term
                   | (force 𝑀)     force execution of a term
-                  | (constr 𝑘 𝑀₀ … 𝑀ₘ₋₁)  constructor with tag 𝑘 and 𝑚 arguments
-                  | (case 𝑀 𝑁₀ … 𝑁ₘ₋₁)    case analysis with 𝑚 alternatives
-                  | (error)     error
+                  | (constr 𝑘 𝑀₁ … 𝑀ₘ)  constructor with tag 𝑘 and 𝑚 arguments (𝑚 ≥ 0).
+                                           Available since 1.1.0
+                  | (case 𝑀 𝑁₁ … 𝑁ₘ)    case analysis with 𝑚 alternatives (𝑚 ≥ 0).
+                                           Available since 1.1.0
+                  | (error)        error
 
 𝑃 ∈ Program ::= (program 𝑣 𝑀)  versioned program
 ```
 
-Plutus (Untyped Plutus Core) is untyped in the sense that variables don't have type tags, and the same variable can have different types during evaluation.
+Plutus (Untyped Plutus Core) is untyped in the sense that variables don't have type tags.
 Constants, however, do carry type tags.
-A constant must be of a builtin type.
-Builtin types and functions are listed in [Builtin Types and Functions](./builtin.md).
+A constant must be of a built-in type.
+Built-in types and functions are listed in [Built-in Types and Functions](./builtin.md).
 
 ## Version Numbers
 
-The 𝑣 in a program is the _Plutus Core language version_.
+The 𝑣 in a program is the _Plutus Core language version_, in the form of `x.y.z`.
 This is distinct from the Plutus ledger language version.
 For a detailed explanation, see [Different Notions of Version](https://plutus.cardano.intersectmbo.org/docs/essential-concepts/versions).
 
@@ -44,9 +46,11 @@ The Haskell definition uses `Word64` for the tag.
 ## de Bruijn Indices
 
 Variable `𝑥` in the above listing can be either textual strings or de Bruijn indices.
-de Bruijn indices are used in serialized scripts.
+De Bruijn indices are used in serialized scripts.
 It therefore makes the most sense for a CEK machine implementation to use de Bruijn indices.
 
+When using de Bruijn indices, the binder `𝑥` in `(lam 𝑥 𝑀)` is irrelevant, and any number can be used.
+
 ## The `data` Type
 
 We provide a built-in type, `data`, which permits the encoding of simple data structures