Lean, show me the first 5 elements in the set of natural num

Stream: Is there code for X?

[Bassem Safieldeen]

When I think about the set of natural numbers its icon in my mind's file system looks something like this: {1, 2, 3, 4, 5, ...}.
When I think about the set of integers its icon looks something like this: {..., -3, -2 -1, 0, 1, 2, 3, ...}.

Is there an easy way to ask Lean to do the same -- to generate a few "nice" elements of a set and show them to me so that I can picture the set better? I would like to apply this to see what the elements of the 2ℤ ideal that I have defined look like.

[Johan Commelin]

At the moment there is not really a machine for doing that.

[Johan Commelin]

I've been thinking a while ago that it would be nice to have "examples" of terms in given types. And tactics could try to combine those.

[Johan Commelin]

But we don't have any framework for this atm.
(Note that example is not the kind of thing I was thinking of.)

[Chris Hughes]

Potentially if you provided a decidable instance for being in the ideal, then there is a proof that the integers are enumerable and that subsets of enumerable types are enumerable so you could use that to show you some elements.

[Bassem Safieldeen]

Chris Hughes said:

Potentially if you provided a decidable instance for being in the ideal, then there is a proof that the integers are enumerable and that subsets of enumerable types are enumerable so you could use that to show you some elements.

Sorry, I don't understand "a decidable instance for being in the ideal".

[Johan Commelin]

It means that you need to write an algorithm that decides whether a given integer is element of the ideal.

[Mario Carneiro]

This sounds kind of like quickcheck, which uses typeclasses for generating representative elements of a variety of types

[Simon Hudon]

It's in the pipes

[Simon Hudon]

I just need write tutorials and documentation for it to be merged