Zulip Chat Archive

Stream: maths

Topic: Defining a function on an inductive type


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 09:19):

Yes, more or less

view this post on Zulip Kenny Lau (Oct 18 2020 at 09:19):

you can see #print list.length

view this post on Zulip Mario Carneiro (Oct 18 2020 at 09:19):

You can see the actual definition with #print

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 09:35):

it's just another identifier character

view this post on Zulip 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'

view this post on Zulip Mario Carneiro (Oct 18 2020 at 09:36):

(actually it's usually just [])

view this post on Zulip 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

view this post on Zulip Golol (Oct 18 2020 at 09:40):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:01):

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

view this post on Zulip Eric Wieser (Oct 18 2020 at 12:27):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 12:33):

probably in the PR that introduced it :P

view this post on Zulip 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