Zulip Chat Archive

Stream: new members

Topic: Recursion with a different argument


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)  := _

view this post on Zulip 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?

view this post on Zulip 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