What does "unfold" mean?

Stream: new members

[mars0i]

What does "unfold" mean? FPIL and TPIL4 regularly speak of unfolding, but as far as I can see, neither defines this term. I tried the Lean 4 manual and the API docs, too.

I gather that it means something like evaluate, reduce, expand, substitute definitions of--something like that. But it seems to be an important concept for Lean, so I'd like to understand it more clearly. (I've been programming for many years, and recently I learned Idris and a little bit of Agda, but I don't recall seeing this term before starting to learn Lean. It's probably not used only for Lean, but a full web search is going to be difficult.)

[Henrik Böving]

"Replace a term with its Definition"

[Markus Schmaus]

In case you don't know yet, Mathlib has a #help command which provides some information on tactics.

import Mathlib
#help tactic unfold

[mars0i]

No, didn't know! Thanks @Markus Schmaus.