Skip to content

Commit aaa0ccc

Browse files
kim-emclaude
andcommitted
chore(nolints): add docBlame exceptions for auto-generated instInhabited.default
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 77f0e70 commit aaa0ccc

1 file changed

Lines changed: 6 additions & 1 deletion

File tree

scripts/nolints.json

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -224,4 +224,9 @@
224224
["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"],
225225
["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
226226
["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
227-
["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"]]
227+
["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
228+
["docBlame", "Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default"],
229+
["docBlame", "Mathlib.Linter.Flexible.instInhabitedStained.default"],
230+
["docBlame", "Mathlib.Linter.instInhabitedImportState.default"],
231+
["docBlame", "Mathlib.Linter.TextBased.instInhabitedStyleError.default"],
232+
["docBlame", "Mathlib.Linter.instInhabitedFormatError.default"]]

0 commit comments

Comments
 (0)