Definicion_de_la_funcion_identidad.lean

-- Definición de la función identidad
-- ==================================

-- ----------------------------------------------------
-- Ej. 1. Definir la función identidad.
-- ----------------------------------------------------

namespace reservado
variable {X : Type}

def id (x : X) : X :=
x

end reservado