doc: Add explanations to MetavarContext (#1331)

* doc: Add explanations to MetavarContext The explanations were taken from Leo's talk at the ICERM Mathlib porting hackathon. * Update src/Lean/MetavarContext.lean Co-authored-by: Sebastian Ullrich <[email protected]> * add my understanding of what LocalInstances represents * Update src/Lean/MetavarContext.lean Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Leonardo de Moura <[email protected]>
leanprover · Jul 31, 2022 · 68e2627 · 68e2627
1 parent a489bdb
commit 68e2627
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
@@ -219,8 +219,10 @@ we may solve the issue by implementing `isDefEqCheap` that never invokes TC and
 -/
 
 /--
-The LocalInstance stores information that the kernel does not care about, but is still
-important to carry for user-facing reasons about local instances in the LocalContext.
+`LocalInstance` represents a local typeclass instance registered by and for
+the elaborator. It stores the name of the typeclass in `className`, and the
+concrete typeclass instance in `fvar`. Note that the kernel does not care about
+this information, since typeclasses are entirely eliminated during elaboration.
 -/
 structure LocalInstance where
   className : Name
@@ -276,6 +278,8 @@ structure MetavarDecl where
   as soon as `mvarIdPending` has been fully synthesized.
   `fvars` are variables in the `mvarIdPending` local context.
 
+  See the comment below `assignDelayedMVar ` for the rationale of delayed assignments.
+
   Recall that we use a locally nameless approach when dealing with binders. Suppose we are
   trying to synthesize `?n` in the expression `e`, in the context of `(fun x => e)`.
   The metavariable `?n` might depend on the bound variable `x`. However, since we are locally nameless,