Is there a function that takes n and gives the list [0,...,n]? find_consts does not give me anything.
upt
Better known under its notation:
term ‹[0..<3]›
It does not seem to be of the right type:
List.upt :: "nat ⇒ nat ⇒ nat list"
Is there another upt?
It should be nat => nat list I think
Ah I see, it takes the head and the last one.
Makes sense! Vielen Dank!
Yiming Xu said:
It should be nat => nat list I think
Only sets have this version (lessThan
, {..<4}
)
I see. That's nice to know.
Last updated: Mar 09 2025 at 12:28 UTC