mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard

Published 20 hours ago • verified publisher icon avigad

Present tactic unfold

Open giomasce opened this issue 1 year ago • 1 comments

As a beginner, I am finding tactic unfold very handy while I'm not able to "see through definitions" yet. Maybe it could be mentioned at some point, together with its at * variant.

giomasce avatar Apr 24 '23 20:04 giomasce

Thanks! The timing is good -- we will be using and revising MIL this summer, and we will figure out where to work this in.

avigad avatar Apr 24 '23 22:04 avigad