The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Yes, but I don't see any link between complexity and functional
extensionality since convertible functions (without fun ext) can already
have different complexity classes.

Maxime.

On 09/13/16 19:18, Jonathan Leivent wrote:
> 
> 
> On 09/13/2016 01:00 PM, Maxime Dénès wrote:
>> Hi Jonathan,
>>
>> On 09/13/16 17:51, Jonathan Leivent wrote:
>>> it can interfere with the preservation of properties like complexity
>>> between extracted code and the original Coq source.
>> Can you elaborate a bit? I vaguely remember this being discussed on the
>> list at some point, but I forgot what it was about.
>>
>> Thanks!
>>
>> Maxime.
> 
> Yeah - it was a briefly heated discussion a while ago.  I don't recall
> it that well, and I think I was one of the instigators.  My point here
> is not to re-raise it.  But, vaguely, the discussion had to do with
> various proxies for complexity that are not preserved by functional
> extensionality, yet otherwise might be of interest when doing Coq ->
> extracted code.  If instead one is limited to functional extensionality
> only on Prop functions, then the point (whatever it was) is obviously
> moot, as such functions don't contribute to extracted code at all.
> 
> -- Jonathan
>