ForMatUS: Pruebas en Lean de P ∧ Q → Q ∧ P
He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P ∧ Q → Q ∧ P en el que se comentan 13 pruebas en Lean de la fórmula (P ∧ Q → Q ∧ P) 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