## Stream: maths

### Topic: Defining a function on an inductive type

#### Golol (Oct 18 2020 at 09:16):

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 (Oct 18 2020 at 09:19):

Yes, more or less

#### Kenny Lau (Oct 18 2020 at 09:19):

you can see #print list.length

#### Mario Carneiro (Oct 18 2020 at 09:19):

You can see the actual definition with #print

#### Mario Carneiro (Oct 18 2020 at 09:20):

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

#### Mario Carneiro (Oct 18 2020 at 09:20):

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

#### Golol (Oct 18 2020 at 09:25):

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 (Oct 18 2020 at 09:35):

it's just another identifier character

#### Mario Carneiro (Oct 18 2020 at 09:36):

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

#### Mario Carneiro (Oct 18 2020 at 09:36):

(actually it's usually just [])

#### Mario Carneiro (Oct 18 2020 at 09:37):

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 (Oct 18 2020 at 09:40):

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

#### Mario Carneiro (Oct 18 2020 at 10:01):

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 (Oct 18 2020 at 10:01):

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

#### Eric Wieser (Oct 18 2020 at 12:27):

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

#### Mario Carneiro (Oct 18 2020 at 12:33):

probably in the PR that introduced it :P

#### Mario Carneiro (Oct 18 2020 at 12:35):

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

Last updated: May 09 2021 at 10:11 UTC