Abstract Lean eliminators combine the notions of recursion and induction. Put another way, eliminators are used to define functions on an inductive type (such as \(\mathbb N\)). The motive describes what kind of function is being defined. To understand motives, one needs to know about types-dependent-on-terms, a threshold concept (in the language of education) that […]