# Zulip Chat Archive

## Stream: new members

### Topic: why does my def call _main?

#### Chris M (Aug 08 2020 at 03:40):

The following code:

```
def append {α : Type*} : list α → list α → list α
| [] l := l
| (h::t) l := h :: append t l
#print append
```

Generates the following printed message:

```
def append : Π {α : Type u_1}, list α → list α → list α :=
λ {α : Type u_1}, append._main
```

In order to get the full definition, I apparently need to write `#print append._main`

instead, which gives:

```
def append._main : Π {α : Type _aux_param_0}, list α → list α → list α :=
λ {α : Type _aux_param_0} (a a_1 : list α),
a.brec_on
(λ (a : list α) (_F : list.below α a) (a_1 : list α),
(λ (a a_1 : list α) (_F : list.below α a),
a.cases_on (λ (_F : list.below α list.nil), id_rhs (list α) a_1)
(λ (a_hd : α) (a_tl : list α) (_F : list.below α (a_hd :: a_tl)),
id_rhs (list α) (a_hd :: _F.fst.fst a_1))
_F)
a
a_1
_F)
a_1
```

What is this `_main`

object? Why is it used, and do I need to think about it?

#### Kenny Lau (Aug 08 2020 at 03:45):

don't unfold definitions; the only things you need is the API

#### Chris M (Aug 08 2020 at 03:46):

What API do you mean?

#### Chris B (Aug 08 2020 at 03:48):

It's because you defined it using the equation compiler (by using pattern matching syntax). You actually get a couple of definitions that you can see with `#print prefix append`

:

```
append : Π {α : Type u_1}, list α → list α → list α
append._main : Π {α : Type _aux_param_0}, list α → list α → list α
append._main._meta_aux : Π {α : Type _aux_param_0}, list α → list α → list α
append._main.equations._eqn_1 : ∀ {α : Type _aux_param_0} (l : list α), append._main list.nil l = l
append._main.equations._eqn_2 : ∀ {α : Type _aux_param_0} (h : α) (t l : list α), append._main (h :: t) l = h :: append._main t l
append._sunfold : Π {α : Type u_1}, list α → list α → list α
append.equations._eqn_1 : ∀ {α : Type u_1} (l : list α), append list.nil l = l
append.equations._eqn_2 : ∀ {α : Type u_1} (h : α) (t l : list α), append (h :: t) l = h :: append t l
```

The ones with _eqn_ are useful sometimes if you want to explicitly do a rewrite using the definition of a particular branch of your function after like `cases l`

or something.

#### Kenny Lau (Aug 08 2020 at 03:48):

`nil_append`

and `cons_append`

#### Kevin Buzzard (Aug 10 2020 at 12:15):

The first two things you should prove about `append`

are `nil_append`

and `cons_append`

, that is, that `append`

satisfies the two things which define it. If you are lucky the proofs are `rfl`

, and in this case you don't ever need to think about `append._main`

because you just proved the two theorems which completely characterise `append`

.

#### Kevin Buzzard (Aug 10 2020 at 12:17):

Sometimes with a more complex inductive type where pattern matching is done in a more obscure way under the hood, these proofs might not be `rfl`

and then you'll have to dig a bit deeper to find that actually the proof is called `foo.equations._eqn_37`

or whatever

#### Kevin Buzzard (Aug 10 2020 at 12:18):

but I bet nil_append and cons_append (which are `_eqn_1`

and `_eqn_2`

) are provable with `rfl`

Last updated: May 14 2021 at 22:15 UTC