Notation in definitions

Stream: general

[Dominik Muc]

I'm new to Lean and trying to write some formalization on simply typed LC. I wanted to use notation for typing in the inductive type definition. Is there a way of doing this? I've seen this implemented in Rocq using „Reserved” notation.

syntax:40 term:40 " ⊢ " term:50 " : " term:40 : term

inductive HasType : (Env X Δ) → Expr X → Typ Δ → Prop where

  | unit
    : Γ ⊢ .unit : .unit
  -- when i try to use it i get „elaboration function for
  -- `«term_⊢_:_»` has not been implemented”

  | var
    : Γ x = τ
    → HasType Γ (.var x) τ

  | abs
    : HasType (Γ.extend τ1) e τ2
    → HasType Γ (.abs e) (Typ.arr τ1 τ2)

  | app
    : HasType Γ e1 (Typ.arr τ1 τ2)
    → HasType Γ e2 (τ1)
    → HasType Γ (.app e1 e2) τ2

  notation:40 Γ " ⊢ " e:50 " : " τ:40 => HasType Γ e τ

[Dominik Muc]

I looked around in web for some time now and only thing I found is
https://github.com/leanprover/lean3/issues/1149
from almost 10 years ago

[Jakub Nowak]

I've you're using notation, don't use syntax. notation is a sugar for syntax + macro. Also notation shouldn't be indented (though, I guess it still works even if it is).

[Jakub Nowak]

The error came from the fact, that it parsed you're syntax according to what was declared in the first line
syntax:40 term:40 " ⊢ " term:50 " : " term:40 : term, and it ignored notation:40 Γ " ⊢ " e:50 " : " τ:40 => HasType Γ e τ. And if you use syntax, you have to give implementation for this syntax somewhere else in your file.
Iirc you can't use syntax in a file, before you give it's implementation, so I don't think there's a way to use your syntax inside HasType definition. (Actually, I think there is, by referring to HasType by name, but I wouldn't recommend that method)