Rob23oba ee5b652136 doc: add documentation for builtin attributes (#8173) ... This PR adds documentation to builtin attributes like `@[refl]` or `@[implemented_by]`. Closes #8432 --------- Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: David Thrane Christiansen <david@lean-fro.org>		2025-06-11 09:04:37 +00:00
..
Compiler	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Data	feat: server-side for module hierarchy (#8654)	2025-06-11 08:02:18 +00:00
DocString	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
Elab	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Language	fix: SnapshotTree.waitAll (#8532)	2025-05-29 20:12:23 +00:00
Linter	chore: fix spelling mistakes (#8711)	2025-06-10 20:24:28 +00:00
Meta	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Parser	feat: #print sig (#8641)	2025-06-05 09:02:19 +00:00
ParserCompiler
PrettyPrinter	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Server	feat: server-side for module hierarchy (#8654)	2025-06-11 08:02:18 +00:00
Util	feat: lake: use lean --setup (#8447)	2025-06-08 17:42:45 +00:00
Widget	feat: reusable rpc refs (#8105)	2025-06-03 12:35:12 +00:00
AddDecl.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
Attributes.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
AuxRecursor.lean
BuiltinDocAttr.lean	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Class.lean	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Compiler.lean
CoreM.lean	feat: create private aux decls in private contexts	2025-06-03 15:53:05 +02:00
Data.lean
Declaration.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
DeclarationRange.lean	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
DefEqAttrib.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
DocString.lean
Elab.lean
EnvExtension.lean	chore: fix spelling mistakes (#8711)	2025-06-10 20:24:28 +00:00
Environment.lean	chore: fix spelling mistakes (#8711)	2025-06-10 20:24:28 +00:00
Exception.lean	fix: unknown identifier ranges (#8362)	2025-05-22 10:05:31 +00:00
Expr.lean	fix: block potential adversarial exploit of non-aborting assert! (#8560)	2025-05-31 03:14:01 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean	fix: block adversarial exploit of non-aborting assert! (#8559)	2025-05-31 00:08:30 +00:00
Linter.lean	feat: implement "linter sets" that can be turned on as a group (#8106)	2025-05-14 23:30:42 +00:00
LoadDynlib.lean
LocalContext.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
Log.lean
Message.lean	fix: improve error-message hint rendering and API (#8486)	2025-06-01 01:22:09 +00:00
Meta.lean	feat: add labeled subcomponents and helper functions for error messages (#8225)	2025-05-07 21:15:27 +00:00
MetavarContext.lean	doc: fix typo in MetavarDecl docstring (#8069)	2025-04-23 22:00:13 +00:00
Modifiers.lean
MonadEnv.lean	feat: revamp aux decl name generation (#8363)	2025-05-16 14:57:18 +00:00
Namespace.lean
Parser.lean
ParserCompiler.lean
PremiseSelection.lean
PrettyPrinter.lean	fix: don't reset localInstances in delaboration (#8022)	2025-04-19 15:39:16 +00:00
PrivateName.lean	chore: do not use the coercion α → Option α in Init and Std (#8085)	2025-04-24 13:35:01 +00:00
ProjFns.lean
ReducibilityAttrs.lean
Replay.lean
ReservedNameAction.lean	feat: make equational theorems of non-exposed defs private (#8519)	2025-06-04 11:52:08 +00:00
ResolveName.lean	fix: let private names be unresolved in the pretty printer, fix shadowing bug when pp.universes is true (#8617)	2025-06-03 23:37:35 +00:00
Runtime.lean
ScopedEnvExtension.lean
Server.lean
Setup.lean	chore: fix spelling mistakes (#8711)	2025-06-10 20:24:28 +00:00
Structure.lean
SubExpr.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
Syntax.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
ToExpr.lean
ToLevel.lean
Util.lean
Widget.lean