Семинар 9. Механизм локалей в Isabelle. Примеры практического применения инструмента
- 00:15Локали. Синтаксис локалей
- 04:39Полезные команды. Дополнение локали
- 11:30Блоки локальных контекстов. Зависимости между локалями. Импорт локалей
- 16:20Интерпретация локалей. Команда sublocale
- 21:43Интерпретация локалей. Команда interpretation. Ключевое слово rewrites. Команда interpret
- 29:10Верификация алгоритма stablecoin
- 54:56Верификация функционального алгоритма сортировки вставками

