Zulip Chat Archive

Stream: new members

Topic: what is the type of fst?


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

view this post on Zulip Mario Carneiro (Oct 22 2019 at 11:48):

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

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

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

view this post on Zulip Jeremy Avigad (Oct 22 2019 at 16:43):

Thanks, Bryan. I will fix this.

view this post on Zulip Marc Huisinga (Oct 22 2019 at 17:33):

(deleted)

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