Stream: Beginner Questions

Topic: Function gives the list [0,1,2,...,n]


view this post on Zulip Yiming Xu (Feb 04 2025 at 19:00):

Is there a function that takes n and gives the list [0,...,n]? find_consts does not give me anything.

view this post on Zulip Mathias Fleury (Feb 04 2025 at 20:00):

upt

view this post on Zulip Mathias Fleury (Feb 04 2025 at 20:00):

Better known under its notation:
term ‹[0..<3]›

view this post on Zulip Yiming Xu (Feb 04 2025 at 20:02):

It does not seem to be of the right type:
List.upt :: "nat ⇒ nat ⇒ nat list"

view this post on Zulip Yiming Xu (Feb 04 2025 at 20:02):

Is there another upt?

view this post on Zulip Yiming Xu (Feb 04 2025 at 20:03):

It should be nat => nat list I think

view this post on Zulip Yiming Xu (Feb 04 2025 at 20:04):

Ah I see, it takes the head and the last one.

view this post on Zulip Yiming Xu (Feb 04 2025 at 20:05):

Makes sense! Vielen Dank!

view this post on Zulip Mathias Fleury (Feb 04 2025 at 20:09):

Yiming Xu said:

It should be nat => nat list I think

Only sets have this version (lessThan, {..<4})

view this post on Zulip Yiming Xu (Feb 04 2025 at 20:16):

I see. That's nice to know.


Last updated: Mar 09 2025 at 12:28 UTC