The Coq mailing list

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

Hi,


Am Montag, den 08.01.2018, 08:23 +0000 schrieb Merlin Göttlinger:
> sure. My guess would be that I messed up the encoding of the
> hierarchy and the fmap call in the implementation of traverse is
> therefore not resolved to be be the Vector.map call.
> https://gist.github.com/mgttlinger/db35a3748f1dfe68c152678f9a714c06

ah, you are using features I have not played around with (e.g. :>, and
default definitions in a record).

Does it work if you do not give the definition of traverse__ in the
Record definition, and instead give it during your Instance? Where is
your Instance?

> What is the "local go" pattern? A quick google lead me only to things
> related to Go-lang.

There might be a better name. It is the problem that nested recursion
through map defined like

Fixpoint map f xs := match xs with
        | [] => []
        | x :: ys => f x :: map f ys end.

fails but 

Definition map f :=
   fix go xs := match xs with
        | [] => []
     
  | x :: ys => f x :: go ys end.

works.

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

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