From ecba8529ccee3a1fede952ec540cde468312606b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 12 Apr 2024 11:14:31 +0200
Subject: [PATCH] doc: Leo-Henrik retreat doc (#3869)

Part of the retreat Hackathon.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
---
 src/Init/Data/Repr.lean  | 13 +++++++++++++
 src/Init/WF.lean         | 19 +++++++++++++++++++
 src/Lean/Meta/Basic.lean | 38 ++++++++++++++++++++++++++++++++++++++
 3 files changed, 70 insertions(+)

diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 10d2fa7a6ee4..c7043589f1d4 100644
--- a/src/Init/Data/Repr.lean
+++ b/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 parentheses 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
 
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index da0f9c050a2c..84c5f2c69c7c 100644
--- a/src/Init/WF.lean
+++ b/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`, then `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,14 @@ 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.
+
+If the arguments of the recursive calls in a function definition decrease according to
+a well founded relation, then the function terminates.
+Well-founded relations are sometimes called _Artinian_ or said to satisfy the “descending chain condition”.
+-/
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
   | intro (h : ∀ a, Acc r a) : WellFounded r
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index de87b256c102..37e2ae76476f 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/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 metavariables.
+- A `Cache` for caching results of the key `MetaM` operations.
+
+The key operations provided by `MetaM` are:
+- `inferType`, which attempts to automatically infer the type of a given expression.
+- `whnf`, which reduces an expression to the point where the outermost part is no longer reducible
+  but the inside may still contain unreduced expression.
+- `isDefEq`, which determines whether two expressions are definitionally equal, possibly assigning
+  meta variables in the process.
+- `forallTelescope` and `lambdaTelescope`, which 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