Siddharth 68e26278c7 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 <sebasti@nullri.ch> * add my understanding of what LocalInstances represents * Update src/Lean/MetavarContext.lean Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>		2022-07-30 21:24:42 -07:00
..
Compiler	chore: cleanup	2022-07-25 22:39:56 -07:00
Data	doc: some doc strings	2022-07-30 21:18:50 -07:00
Elab	doc: some doc strings	2022-07-30 21:18:50 -07:00
Linter	feat: suffix linter messages with option name	2022-07-29 10:31:19 -07:00
Meta	doc: add some docstrings and docstrings details	2022-07-29 10:30:43 -07:00
Parser	doc: add inductive command doc string	2022-07-30 15:15:16 -07:00
ParserCompiler
PrettyPrinter	refactor: improve FVarId method discoverability	2022-07-25 22:18:58 -07:00
Server	feat: structure field auto-completion	2022-07-30 14:40:21 -07:00
Util	chore: cleanup	2022-07-25 22:39:56 -07:00
Widget	feat: add option pp.showLetValues	2022-07-26 17:53:34 -07:00
Attributes.lean	chore: remove unnecessary french quotes	2022-07-29 20:53:01 -07:00
AuxRecursor.lean	feat: add [elabAsElim] elaboration strategy	2022-07-28 20:08:29 -07:00
Class.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Compiler.lean	feat: add isNoncomputable function for querying whether a given declaration has been marked as "noncomputable" by users	2022-02-16 13:20:31 -08:00
CoreM.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Data.lean
Declaration.lean	chore: remove unnecessary french quotes	2022-07-29 20:53:01 -07:00
DeclarationRange.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Deprecated.lean	feat: add [deprecated] attribute	2022-07-24 18:06:03 -07:00
DocString.lean	feat: elaborate add_decl_doc	2022-07-27 09:58:49 -07:00
Elab.lean	refactor: add Elab/Calc.lean	2022-07-24 13:30:05 -07:00
Environment.lean	doc: add some doc strings at Environment.lean	2022-07-30 15:05:13 -07:00
Eval.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Exception.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Expr.lean	chore: remove redundant data form Expr.Data	2022-07-29 21:25:03 -07:00
HeadIndex.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Hygiene.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
ImportingFlag.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
InternalExceptionId.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
KeyedDeclsAttribute.lean	chore: doc strings at KeyedDeclsAttribute.lean	2022-07-25 12:20:19 -07:00
LazyInitExtension.lean
Level.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Linter.lean	feat: add 'suspicious unexpander patterns' linter	2022-07-29 10:31:19 -07:00
LoadDynlib.lean	feat: replace constant with opaque	2022-06-14 17:02:59 -07:00
LocalContext.lean	chore: doc strings	2022-07-29 21:39:34 -07:00
Log.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Message.lean	chore: style	2022-07-29 12:27:01 -07:00
Meta.lean	feat: add evalTerm and Meta.evalExpr	2022-06-28 19:14:40 -07:00
MetavarContext.lean	doc: Add explanations to MetavarContext (#1331)	2022-07-30 21:24:42 -07:00
Modifiers.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
MonadEnv.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Parser.lean	fix: bound syntax kind at v:(ppSpace ident) etc.	2022-07-07 11:49:35 +02:00
ParserCompiler.lean	chore: use a[i]! for array accesses that may panic	2022-07-02 15:12:05 -07:00
PrettyPrinter.lean	feat: ppCategory	2022-07-15 10:58:29 +02:00
ProjFns.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
ReducibilityAttrs.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
ResolveName.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
Runtime.lean	feat: replace constant with opaque	2022-06-14 17:02:59 -07:00
ScopedEnvExtension.lean	chore: remove unnecessary french quotes	2022-07-29 20:53:01 -07:00
Server.lean
Structure.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
SubExpr.lean	refactor: use computed fields for Expr	2022-07-11 14:19:41 -07:00
Syntax.lean	chore: convert doc/mod comments from /- to /--//-! (#1354)	2022-07-22 12:05:31 -07:00
ToExpr.lean	doc: some doc strings	2022-07-30 21:18:50 -07:00
Util.lean	feat: add HasConstCache	2022-03-15 08:39:48 -07:00
Widget.lean	feat: user widgets	2022-07-25 08:01:27 -07:00