The Coq mailing list

[Jerome Hugues <jhugues AT andrew.cmu.edu>]

Thanks for the suggestion

I tried this, but this still produces the same error on nil => I (see rewrite 
below)
The error changed to

The term "I" has type "True" while it is expected to have type
"All Ps ?l@{ls:=ls0; l0:=nil}".

which is a similar error message with different variable names due to the 
renaming

Fixpoint componentInstance_ind' (c : componentInstance) : Pc c :=
  match c with
  | component_instance n ls =>
    component_case n ls
    ((fix subcomponentInstance_ind (ls : list subcomponentInstance) : All 
(Ps) (ls) :=
      match ls with
      | nil => I (* True *) (* All Ps nil *)
      | subcomponent_instance _ c' :: ls' => (componentInstance_ind' c') /\
          (subcomponentInstance_ind ls')
      end)
    ls)
end.

On 1/29/21, 5:14 PM, "coq-club-request AT inria.fr on behalf of Gaëtan Gilbert" 
<coq-club-request AT inria.fr on behalf of gaetan.gilbert AT skyskimmer.net> wrote:

    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) :=
    >