The Coq mailing list

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

Hi Randy,

2016-08-24 0:36 GMT+02:00 Randy Pollack 
<rpollack0 AT gmail.com>:
> I define a function using a measure, e.g.
>
>    Function foo (xs:list nat) : nat :=
>      match xs with  ... end.

Just to be sure: If you use a measure then "{measure lt xs}" should
appear somewhere.

> 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."

That should not happen. Is there some warning? (look in the *coq*
buffer in PG, in case it got hidden somehow)

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

Nothing special there, "Defined" is fine as usual.

Best regards,
Pierre
PS. Can you send the code please, either to coq-club or to me?


>
> Thanks for any help.
>
> --Randy