coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification
Date: Thu, 8 Jun 2017 09:20:48 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f179.google.com
Ironport-phdr: 9a23:3ODpRRBe0ykG79bwmQLNUyQJP3N1i/DPJgcQr6AfoPdwSPvypMbcNUDSrc9gkEXOFd2CrakV1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoINTA5/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kc4YAFOoBPedDr4n9uVQOrga1CBWqBOz1zD9Hm2L90Kog3Os6EQHG3RcgH9IQv3TXttn6LqESXvqzzKbV1znDbvJW2Svy6IXTfRAhpOuDXbN0ccbL1UYvEAbFg0yWpIf4MT2V0eENvHKa7+pmTe+vimgnqxtwoje13MsshJPJi4QIwV7H7SV02Jg5KcG8RUJhYtOpEIFcuz+HO4Z0WM8uXmNltSI8x7Ybo5C0ZjIKx44ixxPHa/yIbYyI4hX7WeaUOzh4hXZldKuihxmo7USs0+P8WtS23VtOtCZFnd7MtncC1xzX9MeLUOdy/kCk2TqX1gDT7P9LIVwsmKbFN5IsxqQ8m5kTvEjZACP6hUf7gLWLekgm/uWk8+Hnba/npp+YOY90kAb+MqE2l8OlGus4MgkOX3Ob+eui173v51f2QLNQgf0wj6bVqpHaJcUHpq62GAJV3YMj5Ay+DzeiytgXgX4HLFdddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd81gogZQCeEBrKTGKLUq16BoOw1dbqifogQ7R/3K/k+5/PtxVY/kFkRNf2g15sWc3C1HbJvJUyfbTztg8sOOWgPtws6CuftjQvRAnZoe3+uUvdktXkAA4W8ANKbSw==

The problem is that it should then reject many good definitions (take division, for instance).

I don't think so. Here is some previous discussion on this topic

Question: https://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00012.html

Answer: https://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00013.html

[Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Gaetan Gilbert, 06/08/2017
  - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
    - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Abhishek Anand, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Morrisett, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
  - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
    - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
  - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
  - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Pierre-Marie Pédrot, 06/08/2017
    - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
      - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017