Search code examples
isabelle

Writing the list of first n natural numbers as ints in Isabelle

I need a list describing a range such as in:

[0..<length P]

However this has type nat list. I later need its type to be int list.

How can I do such a conversion?

Solution

  • The easiest way is probably map int [0..<length p]. In fact, if you just write down [0..<length p] Isabelle might well insert that as a coercion automatically.

    It is a bit unfortunate that this notation only exists for nat; I suppose it is simply not used very often. The equivalent notation for sets ({a..<b} etc.) is much more flexible.