Zulip Chat Archive

Stream: new members

Topic: Fixed arguments in recursive calls

Pedro Minicz (Sep 28 2020 at 18:35):

Is there a way to fix a function argument only to some recursive calls?

Currently I have this:

@[simp] def rename : (  )  term  term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

And would prefer to have something like this:

@[simp] def rename (ρ :   ) : term  term
| (app M N) := app (rename M) (rename N)
| (lam M)   := lam (@rename ρ M)
| (var x)   := var (ρ x)

Mario Carneiro (Sep 28 2020 at 19:23):

You could make it implicit, but if you want to change the value in the recursion then it has to be right of the colon

Last updated: Dec 20 2023 at 11:08 UTC