coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] type coercions

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] type coercions
Date: Tue, 30 Dec 2014 11:01:41 -0800

Is it possible to do something like this:

Program Definition test0 {A B:Type} {H:A=B} (a:A) : B := a.

I would like using 'H' cast (coerce?) 'a' to type 'B'.
Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

[Coq-Club] type coercions, Vadim Zaliva, 12/30/2014
- Re: [Coq-Club] type coercions, Guillaume Melquiond, 12/30/2014
  - Re: [Coq-Club] type coercions, Cedric Auger, 12/30/2014