doc: Leo-Henrik retreat doc

src/Init/Data/Repr.lean

@@ -13,11 +13,24 @@ open Sum Subtype Nat
 
 open Std
 
+/--
+A typeclass that specifies the standard way of turning values of some type into `Format`.
+
+When rendered this `Format` should be as close as possible to something that can be parsed as the
+input value.
+-/
 class Repr (α : Type u) where
+  /--
+  Turn a value of type `α` into `Format` at a given precedence. The precedence value can be used
+  to avoid parenthesis if they are not necessary.
+  -/
   reprPrec : α → Nat → Format
 
 export Repr (reprPrec)
 
+/--
+Turn `a` into `Format` using its `Repr` instance. The precedence level is initially set to 0.
+-/
 abbrev repr [Repr α] (a : α) : Format :=
   reprPrec a 0
 

src/Init/WF.lean

@@ -9,7 +9,18 @@ import Init.Data.Nat.Basic
 
 universe u v
 
+/--
+`Acc` is the accessibility predicate. Given some relation `r` (e.g. `<`) and a value `x`,
+`Acc r x` means that `x` is accessible through `r`:
+
+`x` is accessible if there exists no infinite sequence `... < y₂ < y₁ < y₀ < x`.
+-/
 inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
+  /--
+  A value is accessible if for all `y` such that `r y x`, `y` is also accessible.
+  Note that if there exists no `y` such that `r y x`, `x` is accessible, such an `x` is called a
+  base case.
+  -/
   | intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x
 
 noncomputable abbrev Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
@@ -31,6 +42,13 @@ def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
 
 end Acc
 
+/--
+A relation `r` is `WellFounded` if all elements of `α` are accessible within `r`.
+If a relation is `WellFounded`, it does not allow for an infinite descent along the relation.
+
+This is used to prove that a recursive function, where the arguments of the recursive calls
+decrease according to a well founded relation, terminates.
+-/
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
   | intro (h : ∀ a, Acc r a) : WellFounded r
 

src/Lean/Meta/Basic.lean

@@ -301,6 +301,44 @@ structure Context where
     Note that we do not cache results at `whnf` when `canUnfold?` is not `none`. -/
   canUnfold?        : Option (Config → ConstantInfo → CoreM Bool) := none
 
+/--
+The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
+construction and manipulation, of expressions (`Lean.Expr`) within Lean.
+
+It builds on top of `CoreM` and additionally provides:
+- A `LocalContext` for managing free variables.
+- A `MetavarContext` for managing meta variables.
+- A `Cache` for chaching results of the key `MetaM` operations.
+
+The key operations provided by `MetaM` are:
+- `inferType`, it attempts to automatically infer the type of a given expression.
+- `whnf`, it reduces an expression to the point where the outermost part is no longer reducible
+  but the inside may still contain unreduced expression.
+- `isDefEq`, it determines whether two expressions are definitionally equal, possibly assigning
+  meta variables in the process.
+- `forallTelescope` and `lambdaTelescope`, they make it possible to automatically move into
+  (nested) binders while updating the local context.
+
+The following is a small example that demonstrates how to obtain and manipulate the type of a
+`Fin` expression:
+```
+import Lean
+
+open Lean Meta
+
+def getFinBound (e : Expr) : MetaM (Option Expr) := do
+  let type ← whnf (← inferType e)
+  let_expr Fin bound := type | return none
+  return bound
+
+def a : Fin 100 := 42
+
+run_meta
+  match ← getFinBound (.const ``a []) with
+  | some limit => IO.println (← ppExpr limit)
+  | none => IO.println "no limit found"
+```
+-/
 abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the