diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 1b83f27324..923620c3f2 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -291,36 +291,53 @@ instance : Inhabited (MVarIdMap α) where
   default := {}
 
 /--
-Lean expressions. This datastructure is used in the kernel and
+Lean expressions. This data structure is used in the kernel and
 elaborator. However, expressions sent to the kernel should not
 contain metavariables.
 
 Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
-We considered using «...», but it is too inconvenient to use. -/
+We considered using «...», but it is too inconvenient to use.
+-/
 inductive Expr where
   /--
-  Bound variables. The natural number is the "de Bruijn" index
-  for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information.
-  Example, the expression `fun x : Nat => forall y : Nat, x = y`
+  The `bvar` constructor represents bound variables, i.e. occurrences
+  of a variable in the expression where there is a variable binder
+  above it (i.e. introduced by a `lam`, `forallE`, or `letE`).
+
+  The `deBruijnIndex` parameter is the *de-Bruijn* index for the bound
+  variable. See [here](https://en.wikipedia.org/wiki/De_Bruijn_index)
+  for additional information on de-Bruijn indexes.
+
+  For example, consider the expression `fun x : Nat => forall y : Nat, x = y`.
+  The `x` and `y` variables in the equality expression are constructed
+  using `bvar` and bound to the binders introduced by the earlier
+  `lam` and `forallE` constructors. Here is the corresponding `Expr` representation
+  for the same expression:
   ```lean
   .lam `x (.const `Nat [])
-    (.forall `y (.const `Nat [])
-      (.app (.app (.app (.const `Eq [.succ .zero])
-                  (.const `Nat [])) (.bvar 1))
-            (.bvar 0))
+    (.forallE `y (.const `Nat [])
+      (.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0))
       .default)
     .default
   ```
   -/
   | bvar (deBruijnIndex : Nat)
+
   /--
-  Free variable. Lean uses the locally nameless approach.
-  See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details.
-  When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables
-  are converted into free variables using a unique identifier, and their user-facing name, type,
-  value (for `LetE`), and binder annotation are stored in the `LocalContext`.
+  The `fvar` constructor represent free variables. These /free/ variable
+  occurrences are not bound by an earlier `lam`, `forallE`, or `letE`
+  contructor and its binder exists in a local context only.
+
+  Note that Lean uses the /locally nameless approach/. See [here](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf)
+  for additional details.
+
+  When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`),
+  bound variables are converted into free variables using a unique identifier,
+  and their user-facing name, type, value (for `LetE`), and binder annotation
+  are stored in the `LocalContext`.
   -/
   | fvar (fvarId : FVarId)
+
   /--
   Metavariables are used to represent "holes" in expressions, and goals in the
   tactic framework. Metavariable declarations are stored in the `MetavarContext`.
@@ -328,50 +345,61 @@ inductive Expr where
   or in the code generator.
   -/
   | mvar (mvarId : MVarId)
+
   /--
-  `Type u`, `Sort u`, `Prop`.    -
+  Used for `Type u`, `Sort u`, and `Prop`:
   - `Prop` is represented as `.sort .zero`,
   - `Sort u` as ``.sort (.param `u)``, and
   - `Type u` as ``.sort (.succ (.param `u))``
   -/
   | sort (u : Level)
+
   /--
-  A (universe polymorphic) constant. For example,
-  `@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
-  `@Array.map.{0, 0}` is represented as ``.const `Array.map [.zero, .zero]``.
+  A (universe polymorphic) constant that has been defined earlier in the module or
+  by another imported module. For example, `@Eq.{1}` is represented
+  as ``Expr.const `Eq [.succ .zero]``, and `@Array.map.{0, 0}` is represented
+  as ``Expr.const `Array.map [.zero, .zero]``.
   -/
   | const (declName : Name) (us : List Level)
+
   /--
-  Function application. `Nat.succ Nat.zero` is represented as
-  ```
-  .app (.const `Nat.succ []) (.const .zero [])
-  ```
+  A function application.
+  For example, the natural number one, i.e. `Nat.succ Nat.zero` is represented as
+  `Expr.app (.const `Nat.succ []) (.const .zero [])`
+  Note that multiple arguments are represented using partial application.
+  For example, the two argument application `f x y` is represented as
+  `Expr.app (.app f x) y`.
   -/
   | app (fn : Expr) (arg : Expr)
+
   /--
-  Lambda abstraction (aka anonymous functions).
-  - `fun x : Nat => x` is represented as
+  A lambda abstraction (aka anonymous functions). It introduces a new binder for
+  variable `x` in scope for the lambda body.
+  For example, the expression `fun x : Nat => x` is represented as
   ```
-  .lam `x (.const `Nat []) (.bvar 0) .default
+  Expr.lam `x (.const `Nat []) (.bvar 0) .default
   ```
   -/
   | lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
+
   /--
-  A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows.
-  Examples:
-  - `forall x : Prop, x ∧ x` is represented as
+  A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may dependent
+  on `a`. Note that this constructor is also used to represent non-dependent arrows
+  where `β` does not depend on `a`.
+  For example:
+  - `forall x : Prop, x ∧ x`:
+  ```lean
+  Expr.forallE `x (.sort .zero)
+    (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
   ```
-  .forallE `x
-     (.sort .zero)
-     (.app (.app (.const `And []) (.bvar 0)) (.bvar 0))
-     .default
-  ```
-  - `Nat → Bool` as
-  ```
-  .forallE `a (.const `Nat []) (.const `Bool []) .default
+  - `Nat → Bool`:
+  ```lean
+  Expr.forallE `a (.const `Nat [])
+    (.const `Bool []) .default
   ```
   -/
   | forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
+
   /--
   Let-expressions. The field `nonDep` is not currently used, but will be used in the future
   by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
@@ -388,29 +416,32 @@ inductive Expr where
   `(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
   The let-expression `let x : Nat := 2; Nat.succ x` is represented as
   ```
-  .letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
+  Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
   ```
   -/
   | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
+
   /--
   Natural number and string literal values. They are not really needed, but provide a more
   compact representation in memory for these two kinds of literals, and are used to implement
   efficient reduction in the elaborator and kernel.
   The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is
-  definitionally equal to
-  ```
-  .app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
+  definitionally equal to:
+  ```lean
+  Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
   ```
   -/
-  | lit     : Literal → Expr
+  | lit : Literal → Expr
+
   /--
   Metadata (aka annotations). We use annotations to provide hints to the pretty-printer,
   store references to `Syntax` nodes, position information, and save information for
   elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
   mark `Expr`s that correspond to inaccessible patterns).
-  Note that `.mdata data e` is definitionally equal to `e`.
+  Note that `Expr.mdata data e` is definitionally equal to `e`.
   -/
   | mdata (data : MData) (expr : Expr)
+
   /--
   Projection-expressions. They are redundant, but are used to create more compact
   terms, speedup reduction, and implement eta for structures.