| .. |
|
Deriving
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
InfoTree
|
feat: add elaborators, completions, and hovers for named errors (#8730)
|
2025-06-18 15:51:34 +00:00 |
|
PreDefinition
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Quotation
|
doc: add documentation for builtin attributes (#8173)
|
2025-06-11 09:04:37 +00:00 |
|
Tactic
|
chore: revert DefEq changes until it has passed proper review (#9254)
|
2025-07-08 14:54:18 +00:00 |
|
App.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Arg.lean
|
feat: improve projection and field-notation errors (#8986)
|
2025-06-26 18:36:47 +00:00 |
|
Attributes.lean
|
|
|
|
AutoBound.lean
|
|
|
|
AuxDef.lean
|
feat: meta phase restrictions
|
2025-06-12 16:36:08 +02:00 |
|
BinderPredicates.lean
|
|
|
|
Binders.lean
|
feat: eliminate letFun support, deprecate let_fun syntax (#9086)
|
2025-06-30 02:10:18 +00:00 |
|
BindersUtil.lean
|
|
|
|
BuiltinCommand.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
BuiltinEvalCommand.lean
|
feat: meta phase restrictions
|
2025-06-12 16:36:08 +02:00 |
|
BuiltinNotation.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
BuiltinTerm.lean
|
feat: do not export private declarations (#8337)
|
2025-06-02 08:01:08 +00:00 |
|
Calc.lean
|
|
|
|
CheckTactic.lean
|
|
|
|
Command.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
ComputedFields.lean
|
chore: make compileDecls and friends take an Array rather than a List (#9257)
|
2025-07-08 16:18:44 +00:00 |
|
Config.lean
|
|
|
|
Declaration.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
DeclarationRange.lean
|
|
|
|
DeclModifiers.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
DeclNameGen.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
DeclUtil.lean
|
|
|
|
DefView.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
Deriving.lean
|
|
|
|
Do.lean
|
chore: for #8914 after stage0 update, part 2 (#8931)
|
2025-06-22 22:40:00 +00:00 |
|
ElabRules.lean
|
|
|
|
ErrorExplanation.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
Eval.lean
|
|
|
|
Exception.lean
|
|
|
|
Extra.lean
|
fix: unknown identifier ranges (#8362)
|
2025-05-22 10:05:31 +00:00 |
|
Frontend.lean
|
feat: server support for new module setup (#8699)
|
2025-06-23 18:00:14 +00:00 |
|
GenInjective.lean
|
|
|
|
GuardMsgs.lean
|
fix: check guard_msgs.diff using .get rather than Options.getBool (#8918)
|
2025-06-21 16:03:31 +00:00 |
|
Import.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
Inductive.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
InfoTree.lean
|
|
|
|
InfoTrees.lean
|
feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457)
|
2025-03-13 15:09:00 +00:00 |
|
InheritDoc.lean
|
chore: follow up on #8173 post-stage0 update (#8722)
|
2025-06-16 09:08:35 +00:00 |
|
LetRec.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Level.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
Macro.lean
|
|
|
|
MacroArgUtil.lean
|
|
|
|
MacroRules.lean
|
|
|
|
Match.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
MatchAltView.lean
|
feat: improve error messages in invalid match alternatives (#8368)
|
2025-05-19 17:40:41 +00:00 |
|
MatchExpr.lean
|
|
|
|
Mixfix.lean
|
|
|
|
MutualDef.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
MutualInductive.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Notation.lean
|
|
|
|
Open.lean
|
|
|
|
ParseImportsFast.lean
|
feat: make private the default in module (#9044)
|
2025-06-28 16:30:53 +00:00 |
|
PatternVar.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
PreDefinition.lean
|
|
|
|
Print.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
Quotation.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
RecAppSyntax.lean
|
|
|
|
RecommendedSpelling.lean
|
refactor: environment extension state splitting (#8653)
|
2025-06-11 12:52:04 +00:00 |
|
SetOption.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
StructInst.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Structure.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Syntax.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
SyntheticMVars.lean
|
refactor: migrate to new ranges (#8841)
|
2025-07-07 12:41:53 +00:00 |
|
Tactic.lean
|
feat: Upstream MPL.SPred.* from mpl (#8928)
|
2025-06-26 11:15:11 +00:00 |
|
Term.lean
|
refactor: migrate all usages of old slice notation (#9000)
|
2025-06-27 18:52:07 +00:00 |
|
Time.lean
|
|
|
|
Util.lean
|
doc: add documentation for builtin attributes (#8173)
|
2025-06-11 09:04:37 +00:00 |
|
WhereFinally.lean
|
feat: where ... finally section to assign leftover goals (#8723)
|
2025-06-20 15:51:28 +00:00 |
