what is the type of fst?

Stream: new members

[agro1986]

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]

It's called prod.fst; presumably the tutorial had the prod namespace open

[Bryan Gin-ge Chen]

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]

@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]

Thanks, Bryan. I will fix this.

[Marc Huisinga]

(deleted)

[agro1986]

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