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