File tree Expand file tree Collapse file tree 1 file changed +1
-29
lines changed
Expand file tree Collapse file tree 1 file changed +1
-29
lines changed Original file line number Diff line number Diff line change @@ -60,20 +60,6 @@ Is rev mod use: false
6060-/
6161#guard_msgs in #eval showExtraModUses
6262
63- /-!
64- Running `attribute` with declarations from an imported module causes a rev use.
65- -/
66-
67- #eval resetExtraModUses
68-
69- attribute [builtin_doc] Int.natCast_add
70-
71- /--
72- info: Entries: []
73- Is rev mod use: true
74- -/
75- #guard_msgs in #eval showExtraModUses
76-
7763/-!
7864`recommended_spelling` records a dependency.
7965-/
@@ -188,7 +174,7 @@ attribute [grind =] List.append
188174
189175/--
190176info: Entries: [import Init.Grind.Attr, public import Init.Prelude]
191- Is rev mod use: true
177+ Is rev mod use: false
192178-/
193179#guard_msgs in #eval showExtraModUses
194180
@@ -266,20 +252,6 @@ Is rev mod use: false
266252-/
267253#guard_msgs in #eval showExtraModUses
268254
269- /-!
270- Resolved constants from syntax quotations get added (here `List.sum` from Init.Data.List.Basic).
271- -/
272-
273- #eval resetExtraModUses
274-
275- def test9 : Lean.MacroM Lean.Syntax := `(List.sum)
276-
277- /--
278- info: Entries: [import Init.Notation, import Init.Coe, import Init.Data.List.Basic]
279- Is rev mod use: false
280- -/
281- #guard_msgs in #eval showExtraModUses
282-
283255/-!
284256Elaboration attributes add dependency on the syntax node kind
285257(here `Lean.Parser.Tactic.done` from Init.Tactics).
You can’t perform that action at this time.
0 commit comments