extend projection notation

Stream: new members

[Horatiu Cheval]

Can the x.1 notation for projections be used for other things? I have

inductive type
| zero : type
| arrow : type → type → type
| times : type → type → type

infix `⊗` : 51 := type.times
infixr `↣` : 50 := type.arrow

inductive term : type → Type
| app {σ τ : type} : term (σ ↣ τ) → term σ → term τ
| projl {σ τ : type} : term (σ ⊗ τ ↣ σ)
| projr {σ τ : type} : term (σ ⊗ τ ↣ τ)

namespace term

def fst {σ τ : type} (x : term $ σ ⊗ τ) : term σ :=  app projl x
def snd {σ τ : type} (x : term $ σ ⊗ τ) : term τ :=  app projr x

variables {σ τ : type} {x : term $ σ ⊗ τ}
#check x.fst

end term

and I'm wondering if I can write x.0 and x.1 for x.fst resp. x.snd