coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Are Prop and Set interchangable?

From: yasu AT yasuaki.com
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Are Prop and Set interchangable?
Date: Sat, 01 Aug 2015 21:56:33 +0900

Hi,

I am currently learning COQ. Why is the sequence below valid? Are Prop and Set terms interchangable?

Variable n : Prop.
Variable f : Set -> nat.
Check (f n).

f n : nat

Regards,
Yasuaki

[Coq-Club] Are Prop and Set interchangable?, yasu, 08/01/2015
- Re: [Coq-Club] Are Prop and Set interchangable?, Gabriel Scherer, 08/01/2015
  - Re: [Coq-Club] Are Prop and Set interchangable?, yasu, 08/02/2015
    - Re: [Coq-Club] Are Prop and Set interchangable?, Kristopher Micinski, 08/02/2015
    - Re: [Coq-Club] Are Prop and Set interchangable?, Yasuaki Kudo, 08/02/2015