Recursion with a different argument

Stream: new members

[Guilherme Espada]

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]

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

[Alex J. Best]

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]

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]

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