square brackets in def

Stream: new members

[Alex Zhang]

open list
#check @head

gives me Π {α : Type u_1} [_inst_1 : inhabited α], list α → α.
How should I interpret the [] here and what is the function of [] here?

[Mario Carneiro]

It is a typeclass argument. It links in to a system for automatically generating such proofs called typeclass inference

[Mario Carneiro]

Here inhabited A means A has a distinguished/default/arbitrary element, and list.head will use that element when the list is empty

[Mario Carneiro]

so when you write list.head ([] : list nat) you will get 0 because 0 is the default element of nat

[Mario Carneiro]

which is supplied by the proof that nat is inhabited, docs#nat.inhabited

[Mario Carneiro]

Since empty is not an inhabited type, however, list.head ([] : list empty) is an error, and it has to be because otherwise it would have type empty which would allow us to prove false

[Mario Carneiro]

Unlike haskell, lean has no ability to "throw an error" instead of evaluating to a value, so this function looks a bit different from haskell's List.head function

[Alex Zhang]

So is _inst_1 in [_inst_1 : inhabited α] nothing more than an identifier?

[Eric Wieser]

Yes, Π {α : Type u_1} [inhabited α], list α → α means the same thing

[Bryan Gin-ge Chen]

(Obligatory #tpil chapter link: https://leanprover.github.io/theorem_proving_in_lean/type_classes.html)