RA2010: Isabelle como un lenguaje funcional
En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede en Isabelle/HOL
- calcular con los números naturales, los números enteros y los booleanos,
- definir funciones mediante composición, condicionales, casos e inducción,
- demostrar propiedades mediante simplificación,
- definir tipos de datos recursivos,
- definir y modificar registros y
- refutar propiedades con QuickCheck.