The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Have not tried running the code, but try `match ls return All _ ls with` instead of `match ls with`.  The error message that you got is saying "I don't know how to figure out what to apply "All" to to get "True"".  Another way of phrasing this issue is that when you write "match ls with ..." it doesn't know whether you want the type of the branches to be in terms of `ls`, or to be in terms of the branch of the match.

Best,

Jason

On Fri, Jan 29, 2021 at 5:22 PM Jerome Hugues <jhugues AT andrew.cmu.edu> wrote:

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