En el vídeo se comentan distintas demostraciones sobre la introducción de la implicación en Lean. La primera es con la táctica intro y las siguientes son simplificaciones de la primera hasta llegar al término de la prueba. Finalmente, se presentan demostraciones automáticas.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo, primero de la serie sobre conectivas lógicas, se comentan distintas demostraciones sobre la eliminación de la implicación en Lean. La primera es hacia atrás con tácticas y las siguientes son simplificaciones de la primera hasta llegar al término de la prueba. Finalmente, se presentan demostraciones automáticas.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
He añadido a la lista Programación funcional con Haskell el vídeo Métodos elementales de definición de funciones en Haskell en el que se estudia cómo definir funciones en Haskell usando los formas básicas: composición, condicionales, guardas y patrones.
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
He añadido a la lista Programación funcional con Haskell el vídeo Tipos y clases en Haskell en el que se presenta una introducción a los tipos y clases de tipos en Haskell. Los objetivos de tema son aprender
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
He añadido a la lista Programación funcional con Haskell el vídeo Introducción a la programación funcional con Haskell (Parte 2 de 2) en el que se presenta un panorama general de la programación funcional y se usa Emacs como entorno de desarrollo,
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.