The Coq mailing list

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

Hi Pierre

Sure, I have a tree data type

Inductive tree {value:Type} : Type :=

  | E : tree

  | N : Info.t → tree → key → value → tree → tree.

and here's min_elt

Fixpoint min_elt t : option kvp :=

  match t with

  | E           => None

  | N _ E k v _ => Some (k, v)

  | N _ l _ _ _ => min_elt l

  end.

where kvp := prod key value

let me peruse the documentation too

Best

Chris

On 31 July 2014 19:33, Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:

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