Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Functional Scheme error "cannot define graph(s)"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Functional Scheme error "cannot define graph(s)"


Chronological Thread 
  • From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Functional Scheme error "cannot define graph(s)"
  • Date: Thu, 31 Jul 2014 11:37:12 +0800

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



Archive powered by MHonArc 2.6.18.

Top of Page