Fix argument with tactic

Stream: new members

[Horatiu Cheval]

I have defined something along the lines below. Then I noticed that in many cases I provide the context.nth i = some σ argument of var simply with by simp, like in the example at the end. Due to this, I want to define some var' to be var in which the second explicit argument is fixed as by simp. Can this be done?

import tactic

@[derive decidable_eq]
inductive type
| ground : type
| arrow : type → type → type

@[reducible]
def context := list type

inductive term : context → type → Type
| var {ctx : context} {σ : type} : Π (i : ℕ), ctx.nth i = some σ → term ctx σ

variables {σ τ : type}
def v₀ : term [σ, τ] σ := term.var 0 (by simp)

[Mario Carneiro]

Notations can do that:

notation `#` n := term.var n (by simp)

variables {σ τ : type}
def v₀ : term [σ, τ] σ := #0

[Horatiu Cheval]

Right, thanks!