doc: fix typos (#3114)

src/Lean/Elab/BuiltinNotation.lean

@@ -241,7 +241,8 @@ where
 
 /--
   Helper method for elaborating terms such as `(.+.)` where a constant name is expected.
-  This method is usually used to implement tactics that function names as arguments (e.g., `simp`).
+  This method is usually used to implement tactics that take function names as arguments
+  (e.g., `simp`).
 -/
 def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   let some stx ← liftMacroM <| expandCDotArg? stx | pure none

src/Lean/Meta/InferType.lean

@@ -246,7 +246,7 @@ partial def isPropQuick : Expr → MetaM LBool
   | .mvar mvarId      => do let mvarType  ← inferMVarType mvarId;  isArrowProp mvarType 0
   | .app f ..         => isPropQuickApp f 1
 
-/-- `isProp whnf e` return `true` if `e` is a proposition.
+/-- `isProp e` returns `true` if `e` is a proposition.
 
      If `e` contains metavariables, it may not be possible
      to decide whether is a proposition or not. We return `false` in this
@@ -371,7 +371,6 @@ def isType (e : Expr) : MetaM Bool := do
     | .sort .. => return true
     | _        => return false
 
-
 @[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
   let fvarId ← mkFreshFVarId
   withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do

src/Lean/Util/Trace.lean

@@ -16,7 +16,7 @@ usually as `[class.name] message ▸`.
 Every trace node has a class name, a message, and an array of children.
 This module provides the API to produce trace messages,
 the key entry points are:
-- ``registerTraceMessage `class.name`` registers a trace class
+- ``registerTraceClass `class.name`` registers a trace class
 - ``withTraceNode `class.name (fun result => return msg) do body`
   produces a trace message containing the trace messages in `body` as children
 - `trace[class.name] msg` produces a trace message without children