coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Non strictly positive occurrence

From: Marco Servetto <marco.servetto AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Non strictly positive occurrence
Date: Sun, 22 Aug 2021 09:01:52 +1200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=marco.servetto AT gmail.com; spf=Pass smtp.mailfrom=marco.servetto AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f175.google.com
Ironport-hdrordr: A9a23:vODgsavxouXZHqpvQC0O+PHK7skDe9V00zEX/kB9WHVpm62j5qeTdZEgvyMc5wxhO03I9erhBEDiexLhHPxOkOss1N6ZNWGMhILCFvAG0WKN+UyFJ8Q8zIJgPGVbHpSWxOeeMbGyt6jH3DU=
Ironport-phdr: A9a23:RO8BmBYCoqHRyNe2ld1+aNr/LTE30IqcDmcuAnoPtbtCf+yZ8oj4OwSHvLMx1gePDNyQtq0MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5YHfbx9MiTagbr9/LBe7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+TbxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspXzmp8qVlRwLyiCofODE38G/ZhM9tgqxFvB2svAB/z5LObY2JKPZyYqHQcNUHTmRBRMZRUClBD5u7YYQVFeoOIeFYpJTgqVQQtxu+GxejBP/zyj9Pm3T72qg63P47EQ7a2wwsBckOv2rOrNXrKqgSTfy1zK7TwDXMavNZwzb96IzSfh89pvGMWKt9fMzMwkYgCw3LlE+fqZD5PzyLzOQNtXCW4vduW+6xhGAqtQ98rzqry8oujoTFm4MYx0zZ+St5zog4K9K1RU5mbNOnDZdeuD2WO5Z1T80iXm1ltiQ3xLIIt5O9YSMEy4wnygbBZ/Cbd4WE+BHuWeaLLTtmmH5oe6iziwuw/EWgzOD3S9O630xQriVfl9nBrnAN2ALX6siAUvZ9+12u2TeL1wzK7uFEI104mbPVK5I8wLM9loAfsUvEHi/xl0X2iLGZel849eiv7uTrerTmppmCOI9okgzyLLgil8ilDek7MgUCRXaX9fi/2bH54EH0QrVHguUzkqbDsZDaIcobprS+Aw9Qyosj7gywDy2639Qfh3UHN0xKeAiZj4f3J1HOPPf4AOywg1SpijhrxvTGMqf9DZXKK3jPiK3hcqpl605A1AozyshS6I5TCrEYOf78RkvxtMHDARIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhAszHkbvMh+vTGjHkjmFZbc7P684EQbSWdF+5tJA2ibGDyj8sdFi9euwMkR+usk1CYTzNPe3GaUKc15zV9A4WjW9SQDruxiaCMiX/oVqZdYXpLXwjk+ZbAcoyFX7IIanvXLJY+z3oLUr+uT4Jn3har5leSI19PIe/d+ylevpXmhoAdDwL7mhQ79DgyBMOYgTjlcg==

Dear List, I'm trying to model a problem in COQ but I got stuck. My
minimized problem is the following:

Inductive Bool : Type := | T | F.
Inductive A : Type :=
| myA : (A->Bool)->A.

Error:
Non strictly positive occurrence of "A" in "(A -> Bool) -> A".

I tried various work arounds, but nothing I tried works.
Any ideas? I need ADTs storing functions taking in input the ADT itself.
Marco.

[Coq-Club] Non strictly positive occurrence, Marco Servetto, 08/21/2021
- Re: [Coq-Club] Non strictly positive occurrence, Clément Pit-Claudel, 08/22/2021
  - Re: [Coq-Club] Non strictly positive occurrence, Stefan Monnier, 08/24/2021