## Stream: new members

### Topic: Recursion with a different argument

#### Guilherme Espada (Mar 10 2021 at 15:58):

Given a definition def closed (ctx: ctxtype) : term -> Prop I can define a case with recursion like so: | (t_if cond l r) := closed cond ∧ closed l ∧ closed r.

However, sometimes I want to recurse with a different ctx. How can I do this?

#### Guilherme Espada (Mar 10 2021 at 16:19):

#check closed says closed : ctxtype → term → Prop. It's weird to me how the first parameter gets automatically filled

#### Alex J. Best (Mar 10 2021 at 16:26):

The parameters after the colon are the ones used for matching, so like

def closed : ctxtype -> term -> Prop
| ctx (t_if cond l r)  := _


#### Guilherme Espada (Mar 10 2021 at 16:30):

I understand that, and that does work. However, I never want to match on ctx. Do I have to list it every time if I want to recurse with a different ctx?

#### Alex J. Best (Mar 10 2021 at 16:45):

Can you give an example of what you want to do?
If you don't match it you mean you want to recurse on a completely new ctx?
You don't have to name ctx in the match if you won't use it, you can just put _ instead of ctx but of course you then can't refer to it

Last updated: May 12 2021 at 23:13 UTC