термологический вопрос

[deni_ok]

Коллеги! Не будет ли слишком изощренным издевательством во вводной части обзора Агды, при самом начале обсуждения типа Vec привести такие примеры

[true,false,true] : Vec Bool 3
[2,12,85,0,6] : Vec ℕ 5
Поясню - я не хочу в этом месте вдаваться в детали описания конструкторов, а скрытый здесь грандиозный обман я честным образом раскрою позже.

Comments

[ulysses4ever]

Я Агды не знаю совсем, но пример мне нравится! Интуитивно понятно. Готов потерпеть обман ради такого.

[deni_ok]

на самом деле в Агде все лексемы должны быть отделены друг от друга пробелами. То что стоит слева от каждого оператора типизации (:) - просто идентификатор (причём валидный :)

[ulysses4ever]

А, круто…

[ext_610527]

Сурово. Кто-нибудь на автомате с пробелами напечатает - и твой обман раскроется.

[deni_ok]

так а в любом случае это не валидное замкнутое утверждение, которое можно поселить в модуле. В действительности так

[2,12,85,0,6] : Vec ℕ 5
[2,12,85,0,6] = 2 ∷ 12 ∷ 85 ∷ 0 ∷ 6 ∷ []
Правда тип выражения можно в минибуфере глядеть по C-c C-d