Defining a function on an inductive type

Stream: maths

[Golol]

The eliminator of an inductive type

inductive list (\a : Type u) : Type u+1
| nil : list
| cons (a : \a) (l : list) : list

is the function list.rec_on and it is used to construct functions on lists.
What is going on with this method of defining a function on a list?

def length {α : Type u} : list α → ℕ
| (list.nil' .(α)) := 0
| (list.cons a l) := 1 + length l

Is this syntactic sugar for an application of the recursor?

[Mario Carneiro]

Yes, more or less

[Kenny Lau]

you can see #print list.length

[Mario Carneiro]

You can see the actual definition with #print

[Mario Carneiro]

it's actually more complicated than that because lean compiles to a derived induction principle called list.brec_on

[Mario Carneiro]

but you can look at the definition of this as well and it is all ultimately in terms of list.rec

[Golol]

Thanks!
One more thing: What does the ' symbol do to list.nil here? I've seen that notation a bunch but must've missed the definition.

[Mario Carneiro]

it's just another identifier character

[Mario Carneiro]

That code should not compile with the standard definition of list, because the nil case is spelled list.nil not list.nil'

[Mario Carneiro]

(actually it's usually just [])

[Mario Carneiro]

where did you get that code? We don't usually use inaccessible patterns .(α) anymore, because the elaborator has improved to make them almost always unnecessary

[Golol]

I got it from https://leanprover.github.io/reference/declarations.html 4.4 Inductive types.

[Mario Carneiro]

Ah, it was defined just above as a @[pattern]:

@[pattern]
def list.nil' (α : Type u) : list α := list.nil

def length {α : Type u} : list α → ℕ
| (list.nil' .(α)) := 0
| (list.cons a l) := 1 + length l

[Mario Carneiro]

I think the purpose of this example is just to show off some pattern matching features

[Eric Wieser]

On the note of pattern matching features, is the a@b syntax documented anywhere?

[Mario Carneiro]

probably in the PR that introduced it :P

[Mario Carneiro]

logically it should be in the reference but it doesn't appear to be