can this nesting be implemented in lean?

Stream: new members

[Alok Singh]

def listify : Nat -> ?
| 0        => []
| n + 1    => [listify n]

Is it possible to fill in the '? 'legally?

[Siddhartha Gadgil]

The type depends on n so you cannot. But you can make a dependent function if you want.

[Alok Singh]

can you hint me as to how? implementing it seems useful practice

[Siddhartha Gadgil]

Here is an example

def listType : Nat → Type
  | 0 => List Unit
  | n + 1 => List (listType n)

def listify : (n : Nat) → listType n
  | 0 => []
  | n + 1 => [listify n]

[Alok Singh]

Is there a clean way to do it more inline, without defining a separate function listType?

[Eric Wieser]

Defining the separate type is the cleaner option, but you can write:

def listify : (n : Nat) → n.rec (List Unit) (fun _ x => List x)
  | 0 => []
  | n + 1 => [listify n]

[Alok Singh]

ok yeah the separate way is way better than that

[Eric Wieser]

This also works:

def listify : (n : Nat) → ((by exact List : Function.End _)^(n+1)) Unit
  | 0 => []
  | n + 1 => [listify n]