# Zulip Chat Archive

## Stream: new members

### Topic: unfolding repeating Pi

#### Jesse Michael Han (Sep 21 2018 at 15:11):

hello everyone! i'm trying to define the following inductive datatype:

constant A : Π n : nat, Type inductive hewwo : Type | base : nat → hewwo | apply : Π n, A n → sorry

where the intended type of `apply n f`

is `hewwo →`

... `→ hewwo`

, repeated `n + 1`

times.

I defined the following function:

definition repeat_Pi : ℕ → Type u → Type (u + 1) | 0 A := A | (nat.succ n) A := Π A, repeat_Pi n A

but Lean complains that the following:

inductive hewwo : Type | base : nat → hewwo | apply : Π n, A n → repeat_Pi n hewwo

(rightly) has an incorrect return type for `hewwo.apply`

.

Is there a way to get Lean to treat `repeat_Pi k A`

as being equal to `A -> ... -> A`

?

(edit: got rid of `punit`

and shifted indexing down by 1)

#### Simon Hudon (Sep 21 2018 at 19:46):

Is it intended that in:

... | (nat.succ n) A := Π A, repeat_Pi n A

you ignore `A`

that you get as a parameter?

#### Simon Hudon (Sep 21 2018 at 19:49):

Sorry, that doesn't fix the issue.

You may need to reflect the repetition into the definition of `hewwo`

:

inductive hewwo : nat → Type | base : nat → hewwo 0 | apply (n) : A n → hewwo n → hewwo (succ n)

#### Reid Barton (Sep 21 2018 at 20:37):

@Jesse Michael Han I would just use the uncurried `\Pi n, A n -> (fin n -> hewwo) -> hewwo`

instead.

I don't think you can do the thing you were trying to do.

Last updated: May 14 2021 at 13:24 UTC