The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,

it means that your function is not elligible for functional induction,
either because you have a pattern matching that does not follow the
discipline described in section 2.3 (Function) or because your
function uses higher order too deeply. The error message is explained
in Section 2.3 (we should put a link in the section about Functional
Scheme).

Can you show the definition of min_elt please? It may be easy to fix it.

Best regards,
Pierre


2014-07-31 5:37 GMT+02:00 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