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

[deniok]

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

[true,false,true] : Vec Bool 3
[2,12,85,0,6] : Vec ℕ 5

Поясню - я не хочу в этом месте вдаваться в детали описания конструкторов, а скрытый здесь грандиозный обман я честным образом раскрою позже.

Comments

[alexey bakhirkin (from livejournal.com)]

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

[deni-ok.livejournal.com]

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

[2,12,85,0,6] : Vec ℕ 5
[2,12,85,0,6] = 2 ∷ 12 ∷ 85 ∷ 0 ∷ 6 ∷ []

Правда тип выражения можно в минибуфере глядеть по C-c C-d