§
Big List of Lean4 FAQ
FVar
: free variables
BVar
: bound variables
MVar
: metavariables [variables for unification ].
Lean.Elab.Tactic.*
: tactic front-end code that glues to
Lean.Meta.Tactic.*
.