ForMatUS: Regla de introducción del condicional en Lean
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 la sesión en Lean Web,
- al código,
- al libro “Lógica con Lean” y
- al repositorio en GitHub “Lógica con Lean”.
A continuación, se muestra el vídeo