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 […]

# Tag: Lean 3.30

## Relations in Lean

What is a relation? In a typical undergraduate mathematics course, a relation on a set is defined to be a subset of , the cartesian product of with itself. In the Lean approach, a relation on a type α is a function of type α → α → Prop. That is, a function that takes two terms x and […]