Commit 2024-09-10 10:16 6ff2f9b8

View on Github →

chore(Tactic.StacksAttribute): add kerodon to stacks tag attribute (#16643) Requested for the infinity-cosmos project Zulip

Estimated changes

Modified Mathlib/CategoryTheory/Category/Basic.lean

Modified Mathlib/Tactic/StacksAttribute.lean

deleted def Lean.PrettyPrinter.Parenthesizer.Lean.Environment.getSortedStackProjectDeclNames

deleted def Lean.PrettyPrinter.Parenthesizer.Lean.Environment.getSortedStackProjectTags

added def Lean.PrettyPrinter.Parenthesizer.Mathlib.StacksTag.traceStacksTags

deleted structure Mathlib.Stacks.Tag

deleted def Mathlib.Stacks.addTagEntry

deleted def Mathlib.Stacks.stacksTag

deleted def Mathlib.Stacks.stacksTagFn

deleted def Mathlib.Stacks.stacksTagNoAntiquot

added inductive Mathlib.StacksTag.Database

added structure Mathlib.StacksTag.Tag

added def Mathlib.StacksTag.addTagEntry

added def Mathlib.StacksTag.stacksTagFn

added def Mathlib.StacksTag.stacksTagNoAntiquot

added def Mathlib.StacksTag.stacksTagParser

Modified scripts/noshake.json

Modified test/StacksAttribute.lean