Ejemplo_de_definicion_de_funciones.lean

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función f que le suma 3 a cada número natural.
-- ---------------------------------------------------------------------

def f (x : ℕ) := x + 3

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo de f.
-- ---------------------------------------------------------------------

-- #check f

-- Comentario: Al colocar el cursor sobre check se obtiene
--    f : ℕ → ℕ

-- ---------------------------------------------------------------------
-- Ejercicio 3. Calcular el valor de f(2).
-- ---------------------------------------------------------------------

-- #eval f 2

-- Comentario: Al colocar el cursor sobre eval se obtiene
--    5