The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

You can also be more low level by unfolding eq_rect.

I did not tried it, but I guess that the following would work:

Definition test0 {A B:Type} {H:A=B} (a:A) : B :=
  match H in _=T return T with eq_refl => a end.

I do not know if coq has improved annotations inference. Maybe the following would also work:

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

2014-12-30 20:21 GMT+01:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:

On 30/12/2014 20:01, Vadim Zaliva wrote:

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'.

Definition test0 {A B:Type} {H:A=B} (a:A) : B :=
  eq_rect A (fun C => C) a B H.

Note that, except for a few people, I don't expect anyone to get the formula right on the first try. Here is how I obtained it:

Definition test0 {A B:Type} {H:A=B} (a:A) : B.
Proof.
  rewrite <- H.
  exact a.
Defined.

Best regards,

Guillaume