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

[deniok]

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

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

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

Comments

[deni-ok.livejournal.com]

Да нет, это случайно вышло. Я во введении хотел рассказать общие вещи про зависимые типы, но нужны какие-то примеры. Полезла Agda, ну и следовательно всякие детали синтаксиса. А вдаваться в них там не очень к месту.

Буду думать.