ForMatUS: Reglas de la conjunción en Lean

PorJosé A. Alonso

He añadido a la lista Lógica con Lean el vídeo Reglas de la conjunción en Lean en el que se e comentan 10 demostraciones en Lean que usan las reglas de introducción y eliminación de la conjunción en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático).

Los enlaces correspondientes son:

A continuación, se muestra el vídeo

ForMatUS: Regla de introducción del condicional en Lean

PorJosé A. Alonso

He añadido a la lista Lógica con Lean el vídeo Regla de introducción del condicional en Lean en el que se comentan 13 demostraciones en Lean de la regla de introducción del condicional en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático). Además, se presenta el entorno de trabajo de Lean el de VS Code.

Los enlaces correspondientes son:

A continuación, se muestra el vídeo

ForMatUS: Regla de eliminación del condicional en Lean

PorJosé A. Alonso

He añadido a la lista Lógica con Lean el vídeo Regla de eliminación del condicional en Lean en el que se comentan 7 demostraciones en Lean de la regla de eliminación del condicional en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático). Además,se presenta el entorno de trabajo de Lean en la Red (que permite hacer las pruebas en el navegador sin necesitar ninguna instalación).

Los enlaces correspondientes son:

A continuación, se muestra el vídeo

PFH: Definiciones de tipos en Haskell

PorJosé A. Alonso

He añadido a la lista Programación funcional con Haskell el vídeo Definiciones de tipos en Haskell en el que se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha visto

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando data y
  • cómo definir tipos de datos recursivos usando como ejemplo los naturales, las listas y los árboles.

Se ha insistido en la metodología de definición de funciones recursivas sobre tipos de datos escribiendo una ecuación por cada uno de los constructores del tipo de dato.

El vídeo es

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.