coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [Function] with measure?

From: Randy Pollack <rpollack0 AT gmail.com>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] [Function] with measure?
Date: Tue, 23 Aug 2016 23:36:39 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=rpollack0 AT gmail.com; spf=Pass smtp.mailfrom=rpollack0 AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f43.google.com
Ironport-phdr: 9a23:WMxrlBbDcZ1BRevRbqrFb4//LSx+4OfEezUN459isYplN5qZpcW4bnLW6fgltlLVR4KTs6sC0LuP9fu9EjReqdbZ6TZZIcQKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9JIfegoyN2vyo/NWLOkMT1WP7Ou45dEv+7V2I8JJH2c06cud54yCKi0MAQ/5Ry2JsKADbtDfHzeD0wqRe9T9Nsekq7c9KXPayVa05SbtFEGZuaDhtt4XD/CPORgqX53YaTn5e0l8RW1CEv1nGWcLatTK/ne5g0mGxOdD8BeQ/Xi3n5KN2Qjfpjj0GPng36jeEpNZ3ifdhqRSttlRHxIrQaYqWfK5kZqTZedoRRjJpUcNYVigHCYS5OdhcR9EdNPpV+tGu72AFqgGzUEz1XLvi

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