# Zulip Chat Archive

## Stream: new members

### Topic: what is the type of fst?

#### agro1986 (Oct 22 2019 at 11:41):

Hi everyone! The tutorial https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#function-abstraction-and-evaluation gives example of function fst and snd: "If we have p : nat × nat, then we have fst p : nat"

I tried to "guess" the type of fst so I made fst' (I finished the chapter so I could do an educated guess):

constant fst': Π {α: Type u} {β: Type v}, α × β → α

#check fst' -- ?M_1 × ?M_2 -> ?M_1

#check fst' (1, 2) -- nat

So I then tried to compare it with the fst function mentioned in the tutorial:

#check fst

But I got: unknown identifier 'fst'

My question is:

1) Did I define the type of fst' correctly?

2) What should I do to be able to use fst mentioned in the tutorial?

Thanks a lot.

#### Mario Carneiro (Oct 22 2019 at 11:48):

It's called `prod.fst`

; presumably the tutorial had the `prod`

namespace open

#### Bryan Gin-ge Chen (Oct 22 2019 at 14:42):

The first mention of namespaces in TPiL is in section 2.7, but this question is about the sentence at the beginning of 2.3:

Conversely, if we have

`p : nat × nat`

, then we have`fst p : nat`

and`snd p : nat`

.

Also, while the notations `.1`

and `.2`

are mentioned earlier (at the end of 2.1), the quote above is the first place where `fst`

and `snd`

are mentioned, and then `fst`

and `snd`

don't appear again in this chapter until the end of 2.8 (in the context of `sigma`

). Maybe the above should be changed to "then we have `p.1 : nat`

and `p.2 : nat`

"? @Jeremy Avigad

#### Bryan Gin-ge Chen (Oct 22 2019 at 14:47):

@agro1986 In case this wasn't obvious from what Mario said, the type you gave for `fst'`

is correct. You can check it against what Lean uses with `#check @prod.fst`

.

#### Jeremy Avigad (Oct 22 2019 at 16:43):

Thanks, Bryan. I will fix this.

#### Marc Huisinga (Oct 22 2019 at 17:33):

(deleted)

#### agro1986 (Oct 22 2019 at 18:56):

@Mario Carneiro @Bryan Gin-ge Chen Wow thanks a lot!!!

Last updated: May 13 2021 at 21:12 UTC