Ordinary mathematical functions have a domain and a codomain. In Lean, we write f : α → β to denote that f is a function with domain α and codomain β. More briefly, that f is a function from α to β. The following is a simple example of a function from ℕ to ℤ that we’ve called double. […]