Zulip Chat Archive

Stream: new members

Topic: Inductive Types

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/

Mario Carneiro (Oct 26 2020 at 19:47):

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

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

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.

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

Alex Zhang (Jun 15 2021 at 09:12):

If I define mynat as follows

inductive mynat : Type
| zero : mynat
| succ : mynat  mynat

example : mynat.zero  mynat.succ mynat.zero :=
  intros h,

example : function.injective mynat.succ :=
  intros a b h,

Then do I have "mynat.zero ≠ mynat.succ mynat.zero" and "mynat.succ is injective" by the definition? If so, how can I prove them?

Mario Carneiro (Jun 15 2021 at 09:16):

nat.no_confusion can be used to prove both of them

Mario Carneiro (Jun 15 2021 at 09:17):

the equation compiler knows about both of these lemmas though so you can get some slicker proofs using it

example : mynat.zero  mynat.succ mynat.zero.
example : function.injective mynat.succ | _ _ rfl := rfl

Alex Zhang (Jun 16 2021 at 06:05):

Could you please explain the function of nat.no_confusion?

Kevin Buzzard (Jun 16 2021 at 06:05):


Last updated: Dec 20 2023 at 11:08 UTC