Семинар 6. Объявление типов в Isabelle/HOL. Рекурсивные функции. Индукция
- 00:15Задание типов в Isabelle. Структурная индукция (повторение)
- 13:37Функция, которая переворачивает список (доказательство свойств)
- 31:55Ограничения на структурную индукцию
- 34:31Задание рекурсивных типов (дерево)
- 38:21Функция, которая переворачивает первый список и объединяет его со вторым списком (доказательство свойств)
- 43:36Функция, которая подсчитывает сумму элементов списка из натуральных чисел (доказательство свойств)
- 01:03:28Доказательство утверждений с заданными типами и функциями с помощью индукции (подведение итогов лекции)
