Zulip Chat Archive

Stream: new members

Topic: Why does this following code doesn't type check?


view this post on Zulip Rui Liu (Oct 31 2020 at 12:01):

A beginner question:

#check fun (A: Prop), fun (C:  B: Prop, B), fun (x: (C A)), x

Why does this code doesn't type check? It's complaining at the (C A) part but I don't understand the error message.

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 13:40):

C is a proof that all propositions are true, and C A is a proof that A is true, so it's not a type, so you can't talk about a term x of that type.

view this post on Zulip Rui Liu (Oct 31 2020 at 17:19):

Kevin Buzzard said:

C is a proof that all propositions are true, and C A is a proof that A is true, so it's not a type, so you can't talk about a term x of that type.

Thank you, I see now! An btw the natural number games are fantastic!


Last updated: May 14 2021 at 06:16 UTC