Zulip Chat Archive

Stream: new members

Topic: Variable locality


Wojciech Nawrocki (Feb 11 2019 at 18:37):

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 (Feb 11 2019 at 18:59):

don't use variable names that overlap?

Andrew Ashworth (Feb 11 2019 at 19:00):

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

Wojciech Nawrocki (Feb 11 2019 at 19:06):

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 (Feb 11 2019 at 19:10):

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


Last updated: Dec 20 2023 at 11:08 UTC