The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

As nobody answered, I'll just show you a case I run into lately where an 
identity coercion was needed.

Definition nat_list := list nat.
Record tagged_nat_list := { tag: bool; contents:> nat_list }.
Definition app_nl (x1 x2: nat_list) := app x1 x2.
Fail Definition app_tnl (x1 x2: tagged_nat_list) := app x1 x2.
Identity Coercion _co: nat_list >-> list.
Definition app_tnl (x1 x2: tagged_nat_list) := app x1 x2.

-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France


On Friday 04 November 2011 00:43:34 Victor Porton wrote:
> Honestly I haven't quite understood what are identity coercions.
> 
> Most important I don't understand what is the purpose of identity coercions.
> Why we need special identity coercions, not just plain coercions?