En el vídeo se comentan distintas demostraciones sobre la eliminación de la disyunción en Lean: con tácticas, con término de prueba y 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 se comentan distintas demostraciones sobre la introducción de la conjunción en Lean: con tácticas, con términos de prueba, estructuradas y automática.
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 se comentan distintas demostraciones sobre la eliminación de la conjunción en Lean: con tácticas, con término de prueba, estructuradas y 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 Definiciones de listas por comprensión en Haskell en el que se estudia cómo definir funciones en Haskell usando listas de comprensión. En concreto, hemos visto cómo definir:
También se han estudiados las cadenas como caso particular de listas y cómo aplicar definiciones por comprensión a cadenas.
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
En el vídeo se comentan distintas demostraciones sobre la eliminación de la equivalencia 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. A continuación, se presentan demostraciones estructuradas con razonamiento hacia adelante y, 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