Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual Fixpoints into mutual inductive types


Chronological Thread 
  • From: Joachim Breitner <mail AT joachim-breitner.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Mutual Fixpoints into mutual inductive types
  • Date: Mon, 08 Jan 2018 11:04:16 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
  • Ironport-phdr: 9a23:XxquCxXhurgA15B66tdGEh0gcZfV8LGtZVwlr6E/grcLSJyIuqrYYx2At8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/Ul8J+jLxVrhyjqBxx34HaZ46aOeFxfq/BZ94XX3BMUtpVWiFHH4iyb5EPD+0EPetAq4f9oEEBoge+BQmtAePk1yJFhmXo0q07z+QhFx/J3BY9FN8JtXTbttT1NKMJXOC3y6nH1ynMb/NX2Tf48YTHaQohru+NXbJsd8re11MvGxnYgVqOsIHoOS6e2OoKs2ie9eVgVOSvhnYlqwF2uDeg2scsiojMho4M0V/E7zt2wIcpJd2+VkF7e8SoH4ZOuC2COIt2Q98iQ2F1uCkh0LEJpZm7fC0MxZ86xBDfc+SKf5WK7x/iTuqcJS10iGx4dL+xnRq+7Eatx+P6W8KpylhFtDBFncPJtn0V1xzc9MyHSvxl80ehxzmPzQXT5f9fIUwujqrUNYQhwqAumZoJq0vDGzX5lF/rg6CIbkkk++6o5Pr7Yrj+u5ORNY55hhv6P6g0hMCzHOo1PhITU2WV9+mwzLjj8lf4QLVOgP02iK7ZsJXCKMQevKG5AgtV350h6xa4FTipzNQYnXgCLF5cYx2HlZbmO1DSIPD+E/i/mU6gnyp1yPzeJL3uHo3NLmTfkLfmZbty90lcyBMqwd9D45JUF6oOLenoWk7xsdzYFgU2Pxa1w+bhEtV915kRVXiBAq+DY+vutgqD4ftqKO2RbqcUviz8Ir4r/a3Al3g8zH0adKKp3J5fQmq1H+hgLl/RNX/lg9MpE2ADtQo/SangklCDTThefTC+UvRvtXkAFIu6ANKbFciWi7ub0XLjEw==

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




Archive powered by MHonArc 2.6.18.

Top of Page