coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Function] with measure?

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [Function] with measure?
Date: Tue, 23 Aug 2016 19:01:25 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f172.google.com
Ironport-phdr: 9a23:kglxkBLhWBf2VkNOYNmcpTZWNBhigK39O0sv0rFitYgULfrxwZ3uMQTl6Ol3ixeRBMOAuqsC0Led6vCoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMT2XHkMfsydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+vh7aCACL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOT8TbEvWTmhp45tQRnkwHMOPT4462HaiYp5iqtdrFSgpgBw64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5XAg==

"Grab Existential Variables." may let you make progress on those invisible subgoals.

-- Abhishek
http://www.cs.cornell.edu/~aa755/

On Aug 23, 2016 6:37 PM, "Randy Pollack" <rpollack0 AT gmail.com> wrote:

I define a function using a measure, e.g.

Function foo (xs:list nat) : nat :=
match xs with ... end.

The function is accepted and an obligation goal is generated.

I solve the obligation and the Coq response is

No more subgoals.
(dependent evars:)

Neither Qed nor Defined is accepted at this point, and the function
foo is "not found in the current environment."

I did not find in the RefMan how to finish this definition.

Thanks for any help.

--Randy

[Coq-Club] [Function] with measure?, Randy Pollack, 08/24/2016
- Re: [Coq-Club] [Function] with measure?, Abhishek Anand, 08/24/2016
- Re: [Coq-Club] [Function] with measure?, Pierre Courtieu, 08/24/2016