Notation for inductive types

Stream: lean4

[Tyler Hanks]

Hi I'm fairly new to Lean 4 and I'm trying to figure out if there is a way to define a notation for an inductive type and then use that notation within the definition of that type. For example, if I want to define an inductive type to represent typing judgements in some language, I tried the following:

set_option quotPrecheck false
notation:10 Γ " ⊢ " e " : " t => typing Γ e t

inductive typing : Γ_t → expr → typ → Prop where
  | ttrue : ∀ Γ : Γ_t, Γ ⊢ true_expr : my_bool
  | etc...

But Lean gives me the error unknown identifier 'typing✝' in the ttrue line. Does anyone know any workarounds / solutions for this?

[Sebastian Ullrich]

See e.g. https://github.com/IPDSnelting/tba-2021/blob/b6390e55b768423d3266969e81d19290129c5914/TBA/While/Semantics.lean#L42-L64

[Mario Carneiro]

you can disable quotPrecheck hygiene to forward declare the notation

[Tyler Hanks]

that worked thanks!

[Floris van Doorn]

Did this "feature" get disabled at some point? The following errors:

set_option hygiene false in  -- hacky: allow forward reference in notation
local notation Γ " ⇐ " A => Provable Γ A

inductive Provable : Nat → Nat → Prop
| ax : ∀ {Γ : Nat} {A : Nat}, (Γ ⇐ A) -- error: expected token

[Sebastian Ullrich]

The in creates a new section, so the local notation is short-lived

[Mario Carneiro]

Yeah I ran into this with local attribute as well and was going to report an issue for it. It should use with_weak_namespace or similar

[Floris van Doorn]

Thanks! Removing the in indeed works