Stream: new members
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