doc: Add module docstrings and info about ~q() (#47)

I'm sure much more could be written here, but this makes common patterns in mathlib a little more understandable from the vscode hovers alone.

Qq/Delab.lean

@@ -1,4 +1,8 @@
 import Qq.Macro
+/-!
+# Delaborators for `q()` and `Q()` notation
+-/
+
 open Qq Lean Elab PrettyPrinter.Delaborator SubExpr Meta Impl Std
 
 namespace Qq

Qq/Macro.lean

@@ -2,6 +2,13 @@ import Lean
 import Qq.ForLean.ReduceEval
 import Qq.ForLean.ToExpr
 import Qq.Typ
+/-!
+# The `q( )` and `Q( )` macros
+
+This file provides the main feature of `Qq`; the `q( )` and `Q( )` macros,
+which are available with `open scoped Qq`.
+-/
+
 open Lean Meta Std
 
 namespace Qq

Qq/Match.lean

@@ -2,6 +2,58 @@ import Qq.Macro
 import Qq.MetaM
 import Qq.ForLean.Do
 import Qq.SortLocalDecls
+/-!
+# `~q()` matching
+
+This file extends the syntax of `match` and `let` to permit matching terms of type `Q(α)` using
+`~q(<pattern>)`, just as terms of type `Syntax` can be matched with `` `(<pattern>) ``.
+Compare to the builtin `match_expr` and `let_expr`, `~q()` matching:
+* is type-safe, and so helps avoid many mistakes in match patterns
+* matches by definitional equality, rather than expression equality
+* supports compound expressions, not just a single application
+
+See `Qq.matcher` for a brief syntax summary.
+
+## Matching typeclass instances
+
+For a more complete example, consider
+```
+def isCanonicalAdd {u : Level} {α : Q(Type u)} (inst : Q(Add $α)) (x : Q($α)) :
+    MetaM <| Option (Q($α) × Q($α)) := do
+  match x with
+  | ~q($a + $b) => return some (a, b)
+  | _ => return none
+```
+Here, the `~q($a + $b)` match is specifically matching the addition against the provided `inst`
+instance, as this is what is being used to elaborate the `+`.
+
+If the intent is to match an _arbitrary_ `Add α` instance in `x`,
+then you must match this with a `$inst` antiquotation:
+```
+def isAdd {u : Level} {α : Q(Type u)} (x : Q($α)) :
+    MetaM <| Option (Q(Add $α) × Q($α) × Q($α)) := do
+  match x with
+  | ~q(@HAdd.hAdd _ _ _ (@instHAdd _ $inst) $a $b) => return some (inst, a, b)
+  | _ => return none
+```
+
+## Matching `Expr`s
+
+By itself, `~q()` can only match against terms of the form `Q($α)`.
+To match an `Expr`, it must first be converted to Qq with `Qq.inferTypeQ`.
+
+For instance, to match an arbitrary expression for `n + 37` where `n : Nat`,
+we can write
+```
+def isAdd37 (e : Expr) : MetaM (Option Q(Nat)) := do
+  let ⟨1, ~q(Nat), ~q($n + 37)⟩ ← inferTypeQ e | return none
+  return some n
+```
+This is performing three sequential matches: first that `e` is in `Sort 1`,
+then that the type of `e` is `Nat`,
+then finally that `e` is of the right form.
+This syntax can be used in `match` too.
+-/
 
 open Lean in
 partial def Lean.Syntax.stripPos : Syntax → Syntax
@@ -274,7 +326,40 @@ section
 
 open Impl
 
-scoped syntax "~q(" term ")" : term
+/--
+`Qq`s expression matching in `MetaM`, up to reducible defeq.
+
+This syntax is valid in `match`, `let`, and `if let`, but not `fun`.
+
+The usage is very similar to the builtin `Syntax`-matching that uses `` `(<pattern>)`` notation.
+As an example, consider matching against a `n : Q(ℕ)`, which can be written
+
+* With a `match` expression,
+  ```
+  match n with
+  | ~q(Nat.gcd $x $y) => handleGcd x y
+  | ~q($x + $y) => handleAdd x y
+  | _ => throwError "no match"
+  ```
+* With a `let` expression (if there is a single match)
+  ```
+  let ~q(Nat.gcd $x $y) := n | throwError "no match"
+  handleGcd x y
+  ```
+* With an `if let` statement
+  ```
+  if let ~q(Nat.gcd $x $y) := n then
+    handleGcd x y
+  else if let ~q($x + $y) := n then
+    handleAdd x y
+  else
+    throwError "no match"
+  ```
+
+In addition to the obvious `x` and `y` captures,
+in the example above `~q` also inserts into the context a term of type `$n =Q Nat.gcd $x $y`.
+-/
+scoped syntax (name := matcher) "~q(" term ")" : term
 
 partial def Impl.hasQMatch : Syntax → Bool
   | `(~q($_)) => true

Qq/MetaM.lean

@@ -1,6 +1,13 @@
 import Qq.Macro
 import Qq.Delab
 
+/-!
+# `Qq`-ified spellings of functions in `Lean.Meta`
+
+This file provides variants of the function in the `Lean.Meta` namespace,
+which operate with `Q(_)` instead of `Expr`.
+-/
+
 open Lean Elab Term Meta
 
 namespace Qq
@@ -28,17 +35,35 @@ def elabTermEnsuringTypeQ (stx : Syntax) (expectedType : Q(Sort u))
     TermElabM Q($expectedType) := do
   elabTermEnsuringType stx (some expectedType) catchExPostpone implicitLambda errorMsgHeader?
 
+/--
+A `Qq`-ified version of `Lean.Meta.inferType`
+
+Instead of writing `let α ← inferType e`, this allows writing `let ⟨u, α, e⟩ ← inferTypeQ e`,
+which results in a context of
+```
+e✝ : Expr
+u : Level
+α : Q(Type u)
+e : Q($α)
+```
+Here, the new `e` is defeq to the old one, but now has `Qq`-ascribed type information.
+
+This is frequently useful when using the `~q` matching from `QQ/Match.lean`,
+as it allows an `Expr` to be turned into something that can be matched upon.
+-/
 def inferTypeQ (e : Expr) : MetaM ((u : Level) × (α : Q(Sort $u)) × Q($α)) := do
   let α ← inferType e
   let .sort u ← whnf (← inferType α) | throwError "not a type{indentExpr α}"
   pure ⟨u, α, e⟩
 
+/-- If `e` is a `ty`, then view it as a term of `Q($ty)`. -/
 def checkTypeQ (e : Expr) (ty : Q(Sort $u)) : MetaM (Option Q($ty)) := do
   if ← isDefEq (← inferType e) ty then
     return some e
   else
     return none
 
+/-- The result of `Qq.isDefEqQ`; `MaybeDefEq a b` is an optional version of `$a =Q $b`. -/
 inductive MaybeDefEq {α : Q(Sort $u)} (a b : Q($α)) where
   | defEq : QuotedDefEq a b → MaybeDefEq a b
   | notDefEq : MaybeDefEq a b
@@ -48,12 +73,14 @@ instance : Repr (MaybeDefEq a b) where
     | .defEq _, prec => Repr.addAppParen "defEq _" prec
     | .notDefEq, _ => "notDefEq"
 
+/-- A version of `Lean.Meta.isDefEq` which returns a strongly-typed witness rather than a bool. -/
 def isDefEqQ {α : Q(Sort $u)} (a b : Q($α)) : MetaM (MaybeDefEq a b) := do
   if ← isDefEq a b then
     return .defEq ⟨⟩
   else
     return .notDefEq
 
+/-- Like `Qq.isDefEqQ`, but throws an error if not defeq. -/
 def assertDefEqQ {α : Q(Sort $u)} (a b : Q($α)) : MetaM (PLift (QuotedDefEq a b)) := do
   match ← isDefEqQ a b with
   | .defEq witness => return ⟨witness⟩

Qq/Typ.lean

@@ -49,12 +49,14 @@ structure QuotedLevelDefEq (u v : Level) : Prop :=
   unsafeIntro ::
 
 open Meta in
+/-- Check that a term `e : Q(α)` really has type `α`. -/
 protected def Quoted.check (e : Quoted α) : MetaM Unit := do
   let α' ← inferType e
   unless ← isDefEq α α' do
     throwError "type mismatch{indentExpr e}\n{← mkHasTypeButIsExpectedMsg α' α}"
 
 open Meta in
+/-- Check that the claim `$lhs =Q $rhs` is actually true; that the two terms are defeq. -/
 protected def QuotedDefEq.check (e : @QuotedDefEq u α lhs rhs) : MetaM Unit := do
   α.check
   lhs.check
@@ -63,6 +65,7 @@ protected def QuotedDefEq.check (e : @QuotedDefEq u α lhs rhs) : MetaM Unit :=
     throwError "{lhs} and {rhs} are not defeq"
 
 open Meta in
+/-- Check that the claim `$u =QL $v` is actually true; that the two levels are defeq. -/
 protected def QuotedLevelDefEq.check (e : QuotedLevelDefEq lhs rhs) : MetaM Unit := do
   unless ← isLevelDefEq lhs rhs do
-    throwError "{lhs} and {rhs} are not defeq"
+    throwError "{lhs} and {rhs} are not defeq"