coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Functional Scheme error "cannot define graph(s)", Christopher Ernest Sally, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Pierre Courtieu, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Christopher Ernest Sally, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Pierre Courtieu, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Christopher Ernest Sally, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Pierre Courtieu, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Christopher Ernest Sally, 07/31/2014
- Re: [Coq-Club] Functional Scheme error "cannot define graph(s)", Pierre Courtieu, 07/31/2014
Archive powered by MHonArc 2.6.18.