Can't remove `TacticDoc` linter warning
Closed this issue · 0 comments
kbuzzard commented
On the level-rewrite branch of NNG4 I see the warning
stdout:
./././Game.lean:83:0: warning: Could not find a docstring for tactic decide, consider adding one using `TacticDoc decide "some doc"`
but here it is. What am I doing wrong?