ForMatUS: Reglas de la conjunción en Lean
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 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