En el post sobre Lean como lenguaje de tipos vimos que los tipos inductivos son la construcción para definir nuevos tipos de datos y que se especifican enumerando sus constructores, que son las formas básicas de construir elementos del tipo. Además, cuentan con las reglas de eliminación, que son el mecanismo fundamental que permite definir... Seguir leyendo →