## 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.

(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