## 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