Zulip Chat Archive

Stream: general

Topic: Naming parameters in recursion

Buddy Thunderstuck (Nov 11 2021 at 16:35):

Hello, I have a syntax issue I cannot find anywhere in the reference manual or lean guide. I have a recursive function that takes a list and I need to match the empty list but also have access to the parameter by name (the parameter that is the empty list). Is there a way to do that?

Buddy Thunderstuck (Nov 11 2021 at 16:37):

def recurse : list a -> \list a
| (l : []) := sorry

Kevin Buzzard (Nov 11 2021 at 16:38):

l : [] means "l has type the empty list" which makes no sense because the empty list is not a type. But I don't know how to solve your problem. #xy ? Why do you need a name for something which you know is the empty list? Its name is [].

Buddy Thunderstuck (Nov 11 2021 at 16:43):

Yeah sorry, I know that's incorrect syntax. I thought it might make my question easier to understand. I seem to remember there being syntax for this, something like [] as l
I'll see if I can get away with just using unnamed values and if not, I'll produce an example that is closer to what I'm trying to accomplish. Thanks for your help

Rob Lewis (Nov 11 2021 at 16:46):

def recurse : list a -> \list a
| l@[] := sorry

possibly with parens needed

Buddy Thunderstuck (Nov 11 2021 at 16:52):


Last updated: Dec 20 2023 at 11:08 UTC