max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/stage0/stdlib/Lean
History
Leonardo de Moura dc53fac626
chore: use extensible grind attribute framework to implement [grind] itself (#11769) 
This PR uses the new support for user-defined `grind` attributes to
implement the default `[grind]` attribute.

A manual update-stage0 is required because it affects the .olean files.
2025-12-22 10:07:30 -08:00
..
Compiler chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
Data chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
DocString chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
Elab chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
ErrorExplanations chore: update stage0 2025-12-02 20:03:50 +00:00
Language chore: update stage0 2025-12-17 23:51:56 +00:00
LibrarySuggestions chore: update stage0 2025-12-17 23:51:56 +00:00
Linter chore: update stage0 2025-12-17 23:51:56 +00:00
Meta chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
Parser chore: update stage0 2025-12-22 03:42:18 +00:00
ParserCompiler chore: update stage0 2025-12-17 23:51:56 +00:00
PrettyPrinter chore: update stage0 2025-12-22 03:42:18 +00:00
Server chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
Util chore: update stage0 2025-12-17 23:51:56 +00:00
Widget chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
AddDecl.c chore: update stage0 2025-12-17 23:51:56 +00:00
Attributes.c chore: update stage0 2025-12-17 23:51:56 +00:00
AuxRecursor.c chore: update stage0 2025-12-17 23:51:56 +00:00
BuiltinDocAttr.c chore: update stage0 2025-12-11 15:53:31 +00:00
Class.c chore: update stage0 2025-12-22 03:42:18 +00:00
Compiler.c chore: update stage0 2025-10-23 08:03:18 +00:00
CoreM.c chore: update stage0 2025-12-17 23:51:56 +00:00
Data.c chore: update stage0 2025-10-23 08:03:18 +00:00
Declaration.c chore: update stage0 2025-12-11 15:53:31 +00:00
DeclarationRange.c chore: update stage0 2025-12-11 15:53:31 +00:00
DefEqAttrib.c chore: update stage0 2025-12-17 23:51:56 +00:00
DocString.c chore: update stage0 2025-10-23 08:03:18 +00:00
Elab.c chore: update stage0 2025-12-22 03:42:18 +00:00
EnvExtension.c chore: update stage0 2025-12-11 15:53:31 +00:00
Environment.c chore: update stage0 2025-12-17 23:51:56 +00:00
ErrorExplanation.c chore: update stage0 2025-12-17 23:51:56 +00:00
ErrorExplanations.c chore: update stage0 2025-12-02 20:03:50 +00:00
Exception.c chore: update stage0 2025-12-11 15:53:31 +00:00
Expr.c chore: update stage0 2025-12-22 03:42:18 +00:00
ExtraModUses.c chore: update stage0 2025-12-17 23:51:56 +00:00
HeadIndex.c chore: update stage0 2025-11-28 11:52:39 +00:00
Hygiene.c chore: update stage0 2025-12-11 15:53:31 +00:00
IdentifierSuggestion.c chore: update stage0 2025-12-17 23:51:56 +00:00
ImportingFlag.c chore: update stage0 2025-12-02 20:03:50 +00:00
InternalExceptionId.c chore: update stage0 2025-12-09 15:32:10 +00:00
KeyedDeclsAttribute.c chore: update stage0 2025-12-17 23:51:56 +00:00
LabelAttribute.c chore: update stage0 2025-12-17 23:51:56 +00:00
Level.c chore: use extensible grind attribute framework to implement [grind] itself (#11769) 2025-12-22 10:07:30 -08:00
LibrarySuggestions.c chore: update stage0 2025-11-27 02:33:54 +00:00
Linter.c chore: update stage0 2025-12-12 16:00:39 +00:00
LoadDynlib.c chore: update stage0 2025-12-17 23:51:56 +00:00
LocalContext.c chore: update stage0 2025-12-17 23:51:56 +00:00
Log.c chore: update stage0 2025-12-10 17:28:06 +01:00
Message.c chore: update stage0 2025-12-17 23:51:56 +00:00
Meta.c chore: update stage0 2025-12-15 08:59:34 +00:00
MetavarContext.c chore: update stage0 2025-12-17 23:51:56 +00:00
Modifiers.c chore: update stage0 2025-10-25 11:32:01 +00:00
MonadEnv.c chore: update stage0 2025-12-15 08:59:34 +00:00
Namespace.c chore: update stage0 2025-12-17 23:51:56 +00:00
Parser.c chore: update stage0 2025-12-11 15:53:31 +00:00
ParserCompiler.c chore: update stage0 2025-12-17 23:51:56 +00:00
PrettyPrinter.c chore: update stage0 2025-12-17 23:51:56 +00:00
PrivateName.c chore: update stage0 2025-10-23 08:03:18 +00:00
ProjFns.c chore: update stage0 2025-12-17 23:51:56 +00:00
ReducibilityAttrs.c chore: update stage0 2025-12-17 23:51:56 +00:00
Replay.c chore: update stage0 2025-12-17 23:51:56 +00:00
ReservedNameAction.c chore: update stage0 2025-12-17 23:51:56 +00:00
ResolveName.c chore: update stage0 2025-12-17 23:51:56 +00:00
Runtime.c chore: update stage0 2025-10-23 08:03:18 +00:00
ScopedEnvExtension.c chore: update stage0 2025-12-17 23:51:56 +00:00
Server.c chore: update stage0 2025-10-30 07:41:23 +00:00
Setup.c chore: update stage0 2025-12-17 23:51:56 +00:00
Shell.c chore: update stage0 2025-12-17 23:51:56 +00:00
Structure.c chore: update stage0 2025-12-17 23:51:56 +00:00
SubExpr.c chore: update stage0 2025-12-17 23:51:56 +00:00
Syntax.c chore: update stage0 2025-12-17 23:51:56 +00:00
ToExpr.c chore: update stage0 2025-12-11 15:53:31 +00:00
ToLevel.c chore: update stage0 2025-11-27 03:22:23 +00:00
Util.c chore: update stage0 2025-10-23 08:03:18 +00:00
Widget.c chore: update stage0 2025-10-23 08:03:18 +00:00