coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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: Fri, 05 Jan 2018 19:14:13 +0100
Authentication-results: mail2-smtp-roc.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:KXhoyhzjLxNy8k3XCy+O+j09IxM/srCxBDY+r6Qd1OMRIJqq85mqBkHD//Il1AaPAd2Craocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HObwlSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHrlSkJNyA3/m/Vhcx+kK1Vpx2uqgdww4LIeoyYLuBzcr/fcN4cWGFPXtxRVytEAo6ka4UPCPAOMvpYr4n8olsFsAazBROyC+Pu1j9IgGH53bcn2OkmFAHJxg0gH9YVvXTWq9X6LrsdUeC0zKnN1DnMdOlW1in86IjUdBAuv+uMUahtfsXP0EQiER7OgFuXqYzgJTyV1+INvnCZ7+pnT+2gl24nqwB0ojS23cgskJfGhoMJylDC6yp52pw5KsCmR0Jjbt6kEYdQtyGHN4RtWM8tX2ZouCM8x7YbupC7ZDAHxIklyhPecfCKd5KE7gz+WOufOzt0mXxodby5ih2v60av0Pf8WdOx0FtSripKjN3MtncV2hzT9MeHUP598Vm62TqVzADc9PtEIV4qmqrBMZEhx6Q/moAOvkvdBiP2mUP2g7GKdkg85+Sl6eXqbq/iq5OGKYN4lw/zPr4zlsGxD+k0Kg0OUHKa+eS42r3j50r5QLBSg/0ziKbZsZTaKN8Zpq6+GQBazoYj6xe6Dzu/y9sYh2cILFNZeBKBkYfpIUvCL+3mAvunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4ftoi7vXujHpxs0UQfLWv0IFfPHWxH/BOIUKQanrth5ILC2oLogwzVqrmhQvRAnZoe3+uUvdktXkAA4W8ANKbSw==

Hi,

Am Freitag, den 05.01.2018, 11:54 +0000 schrieb Merlin Göttlinger:
> VectorUtils.traverse depends on a bunch of stuff I implemented and is
> the usual operation known from e.g. Haskell with signature G A -> (A
> -> F B) -> F (G B) where G is (fun T => Vector.t T n) and F is list
> in my case.

Coq’s termination checker cannot look through type class instances.

There is a trick, however, if you get to choose the type class. See
https://github.com/antalsz/hs-to-coq/blob/master/base/GHC/Base.v#L41-L54
and let me know if you want more explanation (I am on the run right
now).

Joachim

--
Joachim Breitner

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

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

[Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
- Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
  - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
    - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Pierre Courtieu, 01/05/2018
    - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
      - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/05/2018
        
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/05/2018
        
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/07/2018
        
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/07/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Merlin Göttlinger, 01/08/2018
        Re: [Coq-Club] Mutual Fixpoints into mutual inductive types, Joachim Breitner, 01/08/2018