The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Dear Club

When using Functional Scheme (with Induction) what does it mean when the system says "cannot define graph(s) for ____"

I have some function min_elt and I'm trying to get my principle with the following

Functional Scheme min_elt_ind := Induction for min_elt Sort Prop.

Thanks very much.

Warm regards

Chris