Variable locality

Stream: new members

[Wojciech Nawrocki]

I noticed that using a variable declaration in inductive type constructors makes them "non-local", in the sense that they apply to the whole type rather than just the constructor, even though they are irrelevant to the type. For example:

section have_this
variable {a: ℕ}
inductive Foo: ℕ → Type
| of_nat: Foo a

#print Foo
/-
inductive Foo : Π {a : ℕ}, ℕ → Type
constructors:
Foo.of_nat : Π {a : ℕ}, Foo a
-/
end have_this

section want_this
inductive Foo': ℕ → Type
| of_nat: Π {a: ℕ}, Foo' a

#print Foo'
/-
inductive Foo' : ℕ → Type
constructors:
Foo'.of_nat : Π {a : ℕ}, Foo' a
-/
end want_this

I would like Lean to generate something like Foo' for me, where only the constructor is a pi-type, but the type being defined is not, but Lean generates Foo, which depends on a resulting in inference errors anywhere. Can I somehow achieve Foo' without explicitly specifying the Pi in every constructor?

[Andrew Ashworth]

don't use variable names that overlap?

[Andrew Ashworth]

alternatively, you might be able to use omit a, but I don't have lean in front of me to check

[Wojciech Nawrocki]

I'm not sure what you mean by overlap? There is no overlap, I simply want a to be added as a Pi-variable to the type of of_nat but not to the type Foo. omit undoes include, but I never had include in the first place. Just to clarify, Foo and Foo' are separate examples - I edited the code to show this.

[Andrew Ashworth]

ah. I don't know the solution to your problem. fixed parameters to the left of the colon ala variable apply to all constructors, so to work around I always explicitly specified the pi type as you did