inconsistency between autoImplicit and variable command

Stream: lean4

[Sebastian Widua]

In an inductive definition when a section variable is used in one constructor, it get's added to all constructors. When using autoImplicit only the used variables are added to each constructor (as I'd expect).
This is pretty annoying when you anything similar to this

variable {x : Nat} {y : Nat}

inductive Foo : Nat → Prop where
  | x : Foo x
  | y : Foo y

the inferrence breaks:

example : Foo 0 := Foo.x
-- fails with “don't know how to synthesize implicit argument 'y'”

[Eric Wieser]

What you wrote means the same thing as

inductive Foo {x : Nat} {y : Nat} : Nat → Prop where
  | x : Foo x
  | y : Foo y

but I assume you meant to write

inductive Foo : Nat → Prop where
  | x {x : Nat} : Foo x
  | y {y : Nat} : Foo y

[Sebastian Widua]

So there's no way to make this less repetitive (with no autoImplicit)?

inductive AExp.Eval : AExp → State → Int → Prop where
  | const {z : Int} {σ : State} : Eval (.const z) σ z
  | var {x : Var} {σ : State} : Eval (.var x) σ (σ x)
  | plus {a₁ a₂ : AExp} {z₁ z₂ : Int} {σ : State} : Eval a₁ σ z₁ → Eval a₂ σ z₂ → Eval (a₁.plus a₂) σ (z₁ + z₂)
  | minus {a₁ a₂ : AExp} {z₁ z₂ : Int} {σ : State} : Eval a₁ σ z₁ → Eval a₂ σ z₂ → Eval (a₁.minus a₂) σ (z₁ - z₂)
  | times {a₁ a₂ : AExp} {z₁ z₂ : Int} {σ : State} : Eval a₁ σ z₁ → Eval a₂ σ z₂ → Eval (a₁.times a₂) σ (z₁ * z₂)

I guess I could let the types be inferred

[Eric Wieser]

Yes, letting the types be inferred is a good middle ground

[Eric Wieser]

Another option if you're really a fan of autoImplicit is set_option autoImplicit true in, which turns it on only for that inductive command.

[Eric Wieser]

You might want to move the State argument before the colon, making it a parameter rather than an index