Написание списка первых n натуральных чисел в виде целых чисел в Изабель

Question

Мне нужен список, описывающий диапазон, например:

[0..<length P]

Однако это имеет тип nat list.Позже мне нужно, чтобы его тип был int list.

Как я могу сделать такое преобразование?

Answer 1

Существует также List.upto со специальным синтаксисом [m..n] для генерации списка целых чисел (тип int list) от m до n (где включены нижняя и верхняя границы включительно). ).

Так что в вашем случае я бы, вероятно, использовал

[0 .. int (length xs) - 1]

(Обратите внимание, что вам все еще нужно преобразование из nat в int для результата length.

Answer 2

Самый простой способ, вероятно, map int [0..<length p]. На самом деле, если вы просто запишите [0..<length p] Изабель вполне может вставить это как принуждение автоматически.

Немного прискорбно, что эта запись существует только для nat; Я предполагаю, что это просто не используется очень часто. Эквивалентная запись для множеств ({a..<b} и т. Д.) Гораздо более гибкая.