This is an implementation of well-scoped lambda calculus terms using Lean, where variables are represented as de Bruijn indices and each term has its context size encoded at the type level. The implementation is presented from the perspective of relative monads, showing that well-scoped lambda calculus terms are an instance of a relative monad of a functor from the category of contexts to the category of sets.
The main inspiration for this work is Altenkirch, T., Chapman, J., & Uustalu, T. (2014). Relative Monads Formalised. Journal of Formalized Reasoning, 7(1), 1–43. https://doi.org/10.6092/issn.1972-5787/4389.