Fixed arguments in recursive calls

Stream: new members

[Pedro Minicz]

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]

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