Commit 2025-10-01 13:25 fd890538

doc(ModelTheory): clarify free and (in-scope) bound variables in BoundedFormula (#29373) The current design of BoundedFormula is actually a locally nameless representation. Following PL convention, we should call the α indexed variables as free variables, and the Fin n indexed variables as (in-scope) bound variables. Also clarify that the bound variables are actually de Bruijn levels. Some references:

• https://jesper.sikanda.be/posts/1001-syntax-representations.html
• Locally nameless in CSLib
• Locally nameless in Lean core