Skip to content

Commit 0133586

Browse files
kim-emkim-em
authored
chore: add #grint_lint exception for sizeOf_spec lemmas (#11300)
1 parent 1aecd85 commit 0133586

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

‎src/Lean/Elab/Tactic/Grind/LintExceptions.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,5 +16,4 @@ import Lean.Elab.Tactic.Grind.Lint
1616
#grind_lint skip List.Sublist.append
1717
#grind_lint skip List.Sublist.middle
1818

19-
-- TODO: restore this after an update-stage0
20-
-- #grind_lint skip suffix sizeOf_spec
19+
#grind_lint skip suffix sizeOf_spec

0 commit comments

Comments
 (0)