Golf explicit list

Stream: general

[Martin Dvořák]

What is the shortest way to write [2, 2, 8, 8, 8, 8, 8, 8, 8, 8, 1, 6, 6, 6, 6, 6, 6] in Lean?

[Yaël Dillies]

import data.list.defs

def sqrepeat (l : list ℕ) : list ℕ := l >>= λ n, list.repeat n n

#eval sqrepeat [2, 8, 1, 6] -- [2, 2, 8, 8, 8, 8, 8, 8, 8, 8, 1, 6, 6, 6, 6, 6, 6]

[Martin Dvořák]

Cool but yours is longer than mine.

[Yaël Dillies]

In terms of characters? I guess you can do

import data.list.defs
#eval[2,8,1,6]>>=λn,list.repeat n n

and that's 59 chars for the entire file.

[Eric Wieser]

It's one character longer but #eval do l←[2,8,1,6],list.repeat l l is also valid syntax for that, in case you didn't know @Martin Dvořák .

[Eric Wieser]

#eval[2,2,8,8,8,8,8,8,8,8,1,6,6,6,6,6,6] is 40 characters...

[Yaël Dillies]

I feel like it should rather be #eval do n←[2,8,1,6],list.repeat n n

[Eric Wieser]

Thankfully both n and l are one character :upside_down:

[Alexandre Rademaker]

What the >>= does?

[Yaël Dillies]

It is docs#has_bind.bind, which here unfolds to docs#list.bind.

[Andrew Yang]

It is the bind operator for the list monad. See wikipedia for more info.