Recursion in weird place

Stream: general

[provemeifyoucan]

Hi there. I managed to get myself to the point when I need to deal with a piece of code that roughly resembles following snippet:

def Eh : Nat -> Type
| Nat.zero => List Unit
| Nat.succ n => List (Eh n)

def rrr : (n:Nat) -> Eh n
| Nat.zero => [()]
| Nat.succ n => let k := rrr n; [k.reverse]

There is a little problem, though, when I give it to lean, it shows me this:

invalid field 'reverse', the environment does not contain 'Eh.reverse'
  k
has type
  Eh n

What can I do to pull myself out of this finicky situation?

[Yaël Dillies]

What's .reverse supposed to refer to? There's no reverse in your code snippet.

[Mauricio Collares]

List.reverse

[Mauricio Collares]

You probably need to unfold Eh at k manually to be able to apply List.reverse

[Mauricio Collares]

Actually this works:

def Eh : Nat -> Type
| Nat.zero => List Unit
| Nat.succ n => List (Eh n)

def rrr : (n:Nat) -> Eh n
| Nat.zero => [()]
| Nat.succ Nat.zero => let k := rrr (Nat.zero); [k.reverse]
| Nat.succ (Nat.succ n) => let k := rrr (Nat.succ n); [k.reverse]

Can you see why Nat.succ Nat.zero and Nat.succ (Nat.succ n) "need" to be handled separately?

[Yaël Dillies]

At that point, k : Eh n is not definitionally of type List α for some α. You need to case on n to get k : List Unit or k : List (Eh m).

[Yaël Dillies]

Well spotted!

[provemeifyoucan]

Thanks for the answer. From now on I will open stuck terms with patterns as "far" as possible XD.
Also, is there a way to make definitions like this def v := Nat.succ v be accepted?

[Yaël Dillies]

partial def v := Nat.succ v

but why do you want that?

[Mario Carneiro]

actually that doesn't work

[Mario Carneiro]

partial defs have to be functions

[Mario Carneiro]

partial def v (_ : Unit) := Nat.succ (v ())

works