(no subject)

Написал кусочек учебника. Модели Скотта. Кто хочет, может сказать, где непонятно и я исправлю

http://www.mediafire.com/download/4f6e8qxkw5cy27f/%D0%BC%D0%BE%D0%B4%D0%B5%D0%BB%D0%B8+%D0%A1%D0%BA%D0%BE%D1%82%D1%82%D0%B0+3.pdf

(no subject)

Agda не даёт использовать \lambda в качестве конструктора! Всякие другие греческие буквы даёт, а лямбду не даёт! А я хотел определить тип "лямбда-термы". Собственно, я потому и взял Агду, что она поддерживает греческие буквы. Обман, всё обман, перейду на Isabelle.