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

Entry tags:

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

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

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

Я считаю, что агдочка достаточно красиво, чтобы её рассказывать без обману! ;-)

Хорошо, так и поступим!

Нет, ну правда — неужели, этот мелкий синтаксический трюк что-то значит?

я уже вполне согласен, что идея была дурацкой

Нет, я буду доказывать! ;-)