The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

This is a bug, it seems to be fixed in trunk.

Meanwhile if you replace curly brackets around {value:Type} by regular
parenthesis it works. Sorry for the inconvenience.

Best regards,
Pierre


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