coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type error for user-defined induction principle for inductive type

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Type error for user-defined induction principle for inductive type
Date: Fri, 29 Jan 2021 23:13:37 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay9-d.mail.gandi.net
Ironport-phdr: 9a23:nRjH8BcrTszbomA5/6CODAz/lGMj4u6mDksu8pMizoh2WeGdxcW7bB7h7PlgxGXEQZ/co6odzbaP4ua7AydZu8zJ8ChbNsAVCFld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6I8xgHHr3dWdOha2H1kKUyOlBr4+su84YRv/itNt/8j7cJMTbn2c6ElRrFEEToqNHw46tf2vhfZVwuP4XUcUmQSkhVWBgXO8Q/3UJTsvCbkr+RxwCaVM9H4QrAyQjSi8rxkSAT0hycdNj4263/Yh8pth69Guh2hphh/w4nJYIGJMfd1Y63Qcc8GSWdHQ81cUTFKDIGhYIsVF+cPIPhWr4f9qVUNoxWxCwajC+HzxTFHnXL2wa433v49HQ3a0gEtHdQDu2nUotXvM6cSVPi4wqjSwjLfc/NZwzH955DJfBAgpfGDRqx/cdDNyUIyEA7FgU+fppL5PzyP0OQBqWeb7+tkVe20lWEnsR1xryO0xscviojJnYEVylHB9SV83ok1P8e0SEhlbt64CZZdsTyROIRqTM04WW5opDo6xaMcuZ69ZCUEyJAqygPBZ/GafIaF4RHuWPuQLDtkgH9od66yihm2/EWj1ODyWcq53UhEoCdEj9TBuXIA2RPX58SaVPZw/Uiv1DCS3A7Q8uFJOV44mbfZJpI7wLM8ioAfvVnAEyL4gkn6kaube0E89uS15enqba/qqoKYOoNulw3zMKAjltaiDek6NgUDWXWQ9/6m273550L5Ra1Hjv0onandt5DXPd4bqbC9AwBP0ocu7w+zACq83NQdh3YHLVZFdAiIj4fzPVHBPfH4Ae25g1uyjDdn3/HGPrv/DZXRNnXPjqrtcLRn50Ne1AY/181T6pFaB70bPf7+Xkv8uMTdDhAjMgy0x+jnCM961oMbQW+PDbWWP73OsVCS4OIjOeaMZI4RuDnmNfcl/eLugGQimV8efaipxpgXaHG9HvRjPUqZe2DggtEfHmcWpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxXHYSmHoQmzFSlsBLw47thNOvdvCMC5rz5090gyORQiRg0whN1C86QyX3FG259k38BQXk53aR1rFZh4kyAwLN7gvldGMYV4f5VBFRpfaXAxvB3XoihEjnKec2EHQ7/E4eWRAopR9d0+OcgJkN0GtGslBfGhnT4GLwEjL+KAZk56OTa0mSjfp8gmUaD77EoihwdeuUKNWCigfQipRLeA4fYwgCV0aOjdKBa0yfL+GbFy2eS7hkBDFxAFJ7dVHVaXXP46Mzj7xqcHaStGK8kMw5ExNTELKZWOIXk

Didn't check but I think

((fix subcomponentInstance_ind (lsi : list subcomponentInstance) : All
(Ps) (ls) :=

should be ... : All Ps lsi, not ... : All Ps ls

Then I would just shadow ls to reduce typo possibilities

Gaëtan Gilbert

On 29/01/2021 22:58, Jerome Hugues wrote:

((fix subcomponentInstance_ind (lsi : list subcomponentInstance) : All
(Ps) (ls) :=

[Coq-Club] Type error for user-defined induction principle for inductive type, Jerome Hugues, 01/29/2021
- Re: [Coq-Club] Type error for user-defined induction principle for inductive type, Gaëtan Gilbert, 01/29/2021
  - Re: [Coq-Club] Type error for user-defined induction principle for inductive type, Jerome Hugues, 01/29/2021
    - Re: [Coq-Club] Type error for user-defined induction principle for inductive type, Jason Gross, 01/30/2021
      - Re: [Coq-Club] Type error for user-defined induction principle for inductive type, Jerome Hugues, 01/30/2021