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