Apply suggestions from code review

Co-authored-by: Jonas Schulze <[email protected]>

Author: Keno

base/expr.jl

@@ -379,7 +379,7 @@ end
 `ex` must be a method definition.
 
 WARNING: Improper use of this macro causes undefined behavior (including crashes,
-incorrect answers, or other hard to track bugs). Use with care an only if absolutely
+incorrect answers, or other hard to track bugs). Use with care and only if absolutely
 required.
 
 In general, each `setting` value makes an assertion about the behavior of the
@@ -400,17 +400,17 @@ Note: This in particular implies that the return value of the method must be
       contents) are not egal.
 
 Note: The idempotency assertion is made world-arge wise. More formally, write
-      fₐ for the evaluation of `f` in world-age `a`, then we require:
+      fᵢ for the evaluation of `f` in world-age `i`, then we require:
 
-          ∀ a, x, y: x === y → fₐ(x) === fₐ(y)
+          ∀ i, x, y: x === y → fᵢ(x) === fᵢ(y)
 
-      However, for two world ages `a, b` s.t. `a != b`, we may have `fₐ(x) !== fₐ(y)``
+      However, for two world ages `i, j` s.t. `i != j`, we may have `fᵢ(x) !== fⱼ(y)`.
 
-Note: A further implication is that idempontent functions may not make their
+Note: A further implication is that idempotent functions may not make their
       return value dependent on the state of the heap or any other global state
       that is not constant for a given world age.
 
-Note: The idempontency includes all legal rewrites performed by the optimizizer.
+Note: The idempotency includes all legal rewrites performed by the optimizizer.
       For example, floating-point fastmath operations are not considered idempotent,
       because the optimizer may rewrite them causing the output to not be idempotent,
       even for the same world age (e.g. because one ran in the interpreter, while
@@ -460,20 +460,20 @@ Note: MethodErrors and similar exceptions count as abnormal termination.
 # `:terminates_globally`
 
 The `:terminates_globally` settings asserts that this method will eventually terminate
-(either normally or abnormally), i.e. does not infinite loop.
+(either normally or abnormally), i.e. does not loop indefinitely.
 
 Note: The compiler will consider this a strong indication that the method will
       terminate relatively *quickly* and may (if otherwise legal), call this
       method at compile time. I.e. it is a bad idea to annotate this setting
       on a method that *technically*, but not *practically*, terminates.
 
-Note: The `terminates_globally` assertion, covers any other methods called by
+Note: The `terminates_globally` assertion covers any other methods called by
       the annotated method.
 
 # `:terminates_locally`
 
 The `:terminates_locally` setting is like `:terminates_globally`, except that it only
-applies to syntactic control flow *within* the annotated method. It is this
+applies to syntactic control flow *within* the annotated method. It is thus
 a much weaker (and thus safer) assertion that allows for the possibility of
 non-termination if the method calls some other method that does not terminate.