Zulip Chat Archive

Stream: new members

Topic: Inductive Types


view this post on Zulip Yasmine Sharoda (Oct 26 2020 at 19:47):

Hello, I am writing my first program in lean. I defined the following inductive type

inductive Expr (A : Type)
| singleton : A -> Expr

Expr is a parameterized type, and so instances would have type Expr A for some type A. But the occurrence of the type Expr in the definition of singleton does not include the parameter? Is their a good reason?
PS: I am type checking this using the online tool: https://leanprover.github.io/live/latest/

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:47):

It does actually have the parameter, as you can see with #print Expr.singleton

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:48):

but in the definition, the parameters to the inductive type are left off so you can't change them

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 19:49):

You're not allowed to use Expr with any other parameter inside | singleton : A → Expr line, so you don't write the parameter at all.

view this post on Zulip Mario Carneiro (Oct 26 2020 at 19:50):

technically speaking, inside the types for the constructors, a local variable called Expr : Type is available for use to refer to the type being defined, and when the constructor is actually created, this variable is replaced with Expr A where Expr : Type -> Type is the new constant


Last updated: May 12 2021 at 04:19 UTC