## Stream: Is there code for X?

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

#### Bassem Safieldeen (Jul 04 2020 at 19:18):

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 (Jul 04 2020 at 19:20):

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

#### Johan Commelin (Jul 04 2020 at 19:20):

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 (Jul 04 2020 at 19:21):

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 (Jul 04 2020 at 19:21):

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 (Jul 04 2020 at 19:25):

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 (Jul 04 2020 at 19:26):

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

#### Mario Carneiro (Jul 04 2020 at 20:01):

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

#### Simon Hudon (Jul 04 2020 at 20:11):

It's in the pipes

#### Simon Hudon (Jul 04 2020 at 20:11):

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

Last updated: May 07 2021 at 19:12 UTC