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: Aug 03 2023 at 10:10 UTC