The Coq mailing list

[劉弘毅 <liukoki AT gmail.com>]

I didn't know that the word "Qed." actually makes the value opaque. Thanks for telling that to me.

On Tue, Sep 29, 2020 at 12:08 AM 劉弘毅 <liukoki AT gmail.com> wrote:

Thanks. Yeah, it seems that I don't have enough understanding of the proofs regarding dependent types yet. I'm gonna get a basic understanding of the field with a textbook, and CPDT seems a good one. Thanks for introducing that to me.

On Mon, Sep 28, 2020 at 11:37 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

You are headed into complex territory here, and I recommend reading a comprehensive introduction, rather than proceeding one question at a time.  I'm biased, but my suggestion is Chapter 10 of CPDT.

On 9/28/20 10:34 AM, 劉弘毅 wrote:

Could I ask you another question? Now, is there a way to show the equivalence of "omega" and "cast"?

I would like to do something like

  omega a = cast a

Since (T (f a)) and (T (g a)) are the different expressions of the same type, these values should be comparable. However, the equation does not type-check.

Moreover, I cannot unfold the "cast" function since it is defined with "Proof" and made opaque. Is it impossible to make this kind of comparison?