lint(lean/main/tactics): remove unused definition

leanprover-community / lean4-metaprogramming-book

Apache License 2.0

211 stars 50 forks source link

Closed adomani closed 1 year ago

adomani commented 1 year ago

I extracted here one of the questions from #79, to group together similar looking one.