I1M2011: Definición de tipos de datos en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha estudiado

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando
  • data y

  • cómo definir tipos de datos recursivos usando como ejemplo los naturales.

Las transparencias usadas en la clase son las del tema 9:
Read More “I1M2011: Definición de tipos de datos en Haskell”

RA2011: Patrones de inducción en Isabelle: casos, inducción y otros

En la clase de hoy del curso de Razonamiento automático se han presentado los principales patrones de inducción en Isabelle: en la primera parte se ha presentado los patrones de de mostración por casos y por inducción y en la segunda parte se han presentado otros patrones (eliminación de disyunción, negación, contradicción y equivalencias).

La primera parte de la clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Patrones de inducción en Isabelle: casos, inducción y otros”