unfolding repeating Pi

Stream: new members

[Jesse Michael Han]

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]

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]

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]

@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.