Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders

Ernesto Copello, Nora Szasz, Álvaro Tasistro

We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then…