The Coq mailing list

[Victor Porton <porton AT narod.ru>]

04.11.2011, 16:50, "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.

I don't understand this:

1. Shouldn't _co be already defined before making it a coercion?

2. I nevertheless don't understand what is an identity coercion, what is its 
difference from plain coercion.

> 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?

-- 
Victor Porton - http://portonvictor.org