Naming parameters in recursion

Stream: general

[Buddy Thunderstuck]

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]

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

[Kevin Buzzard]

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]

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]

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

possibly with parens needed

[Buddy Thunderstuck]

Thanks!