The `{}` annotation for inductive types

Stream: Type theory

[Gihan Marasingha]

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]

implicit arguments

[Kevin Buzzard]

#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]

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

[Gihan Marasingha]

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]

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]

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]

@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]

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

[Kevin Buzzard]

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

[Jeremy Avigad]

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]

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.