The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

On Sat, Feb 22, 2014 at 2:32 PM, Rui Baptista 
<rpgcbaptista AT gmail.com>
 wrote:
> A quick fix is:
>
> Definition implication (P Q : Prop) : Prop := P -> Q.
>
> Function truth' P {measure complexity P} : Prop := match P with
> | atom     => True
> | conn P Q => implication (truth' P) (truth' Q)
> end.

Thanks, that worked. Is there any workaround when the recursive call
is in the body of a lambda? (See example in my other reply some
minutes ago.)