## Stream: Type theory

### Topic: The {} annotation for inductive types

#### Gihan Marasingha (Dec 20 2020 at 15:26):

Can someone give a simple example to show where the {} annotation for constructors of inductive types is necessary? For instance, what works with

inductive sum (α : Type u) (β : Type v)
| inl {} : α → sum
| inr {} : β → sum


that doesn't work for

inductive sum' (α : Type u) (β : Type v)
| inl : α → sum'
| inr : β → sum'


?

#### Kenny Lau (Dec 20 2020 at 15:40):

implicit arguments

#### Kevin Buzzard (Dec 20 2020 at 15:42):

#tpil explains an example here.

...erm, except that indeed the {} (in list.nil) seems to have no effect in their example either.

universes u

namespace hidden

inductive list (α : Type u)
| nil {} : list
| cons : α → list → list

inductive list' (α : Type u)
| nil : list' -- get {} brackets
| cons : α → list' → list'

inductive list'' (α : Type*)
| nil [] : list'' -- get () brackets :D
| cons : α → list'' → list''


#### Kevin Buzzard (Dec 20 2020 at 15:45):

I think some change was made in core Lean relatively recently and perhaps TPIL was not updated.

#### Gihan Marasingha (Dec 20 2020 at 16:11):

Right, that's what I thought. The [] annotation does make a difference, but just removing {} doesn't seem to do anything. Should the definitions in mathlib be updated to remove the {} annotation?

Unless there really is a difference and I just don't understand what it is.

#### Kevin Buzzard (Dec 20 2020 at 16:18):

universes u v

namespace hidden

inductive sum1 (α : Type u) (β : Type v)
| inl {} : α → sum1
| inr {} : β → sum1

inductive sum2 (α : Type u) (β : Type v)
| inl : α → sum2
| inr : β → sum2

#print prefix hidden.sum1
#print prefix hidden.sum2

end hidden


Make the infoview big and move your cursor between the two #print statements to see...no change at all other than 1<->2

#### Gihan Marasingha (Dec 20 2020 at 16:22):

Yes and ignore my previous comment. I see that the constructors for sum and list don't take the {} annotation in core Lean.

#### Gihan Marasingha (Dec 20 2020 at 16:26):

@Jeremy Avigad can you confirm that the {} annotation for constructors of implicit types doesn't do anything in the current version of Lean? Does tpil need to be updated?

#### Kevin Buzzard (Dec 20 2020 at 16:27):

so one can use git blame to find out when that changed, and one is led here.

#### Kevin Buzzard (Dec 20 2020 at 16:32):

Looking at the diff, you see that it was clearly the right decision.

#### Jeremy Avigad (Dec 22 2020 at 17:47):

Sorry, I have been dragging my feet on this. The semester is over now, and my grades are in. Within the next day or two I'll update TPIL to compile with the latest version of mathlib, and I'll update this in the text.

#### Jeremy Avigad (Dec 23 2020 at 02:20):

I just updated TPIL to Lean 3.23.0, removed the discussion of {}, and merged a number of pull requests I had been neglecting. @Gihan Marasingha thanks for pinging me on this.

Last updated: May 08 2021 at 23:10 UTC