The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

Hi Tej,

thanks for looking into it!


Am Freitag, den 03.11.2017, 09:40 -0400 schrieb Tej Chajed:
> I saw this on Stack Exchange and started looking into it. Your first
> question really surprised me - it appears you have dead code that
> helps the termination checker. What’s going on in that the let-bound
> list_C (I’ll call it list_C’ to avoid confusion with the definition
> it shadows) is used for typeclass instantiation rather than the
> global instance.

Right, but that’s my point: list_C and list_C' seem to be mostly
equivalent to me, but somehow using list_C' allows the termination
checker to see through it, which is not the case for list_C!

> So in tree_P2 it’s not evaluation but instead typeclass resolution 
> not actually using the global list_C.

Right. If you compare tree_P2 (which works) and tree_P3 (which does not
work), then the only difference is that I replaced

  list_P 

with

  (@P _ (@list_C _ tree_C) ts)

(using the global tree_C). But the latter should reduce to the former
quite immediately, shouldn’t it?

Joachim
-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part